Quantum CPOs
arXiv:2109.02196 · doi:10.4204/EPTCS.340.9
Abstract
We introduce the monoidal closed category qCPO of quantum cpos, whose objects are "quantized" analogs of omega-complete partial orders (cpos). The category qCPO is enriched over the category CPO of cpos, and contains both CPO, and the opposite of the category FdAlg of finite-dimensional von Neumann algebras as monoidal subcategories. We use qCPO to construct a sound model for the quantum programming language Proto-Quipper-M (PQM) extended with term recursion, as well as a sound and computationally adequate model for the Linear/Non-Linear Fixpoint Calculus (LNL-FPC), which is both an extension of the Fixpoint Calculus (FPC) with linear types, and an extension of a circuit-free fragment of PQM that includes recursive types.
arXiv commentIn Proceedings QPL 2020, arXiv:2109.01534
References in corpus (7)
- A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)
- Classical Control, Quantum Circuits and Linear Logic in Enriched Category Theory
- Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
- Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
- Quantum sets
- Von Neumann Algebras form a Model for the Quantum Lambda Calculus
- Hereditarily antisymmetric operator algebras