Quantum programming with inductive datatypes: causality and affine type theory
From MaRDI portal
(Redirected from Publication:2200848)
Abstract: Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics.
Recommendations
Cites work
- A categorical semantics for causal structure
- A single quantum cannot be cloned
- Applying quantitative semantics to higher-order quantum computing
- Classical control, quantum circuits and linear logic in enriched category theory
- Concurrent quantum strategies
- Enriching a linear/non-linear lambda calculus: a programming language for string diagrams
- LNL-FPC: the linear/non-linear fixpoint calculus
- Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
- Quantum collections
- Quantum Entanglement Analysis Based on Abstract Interpretation
- Quantum programming languages: survey and bibliography
- Quantum Programs as Kleisli Maps
- Semantics for a quantum programming language by operator algebras
- Semantics for a quantum programming language by operator algebras
- Semantics of higher-order quantum computation via geometry of interaction
- The geometry of parallelism: classical, probabilistic, and quantum effects
- Theory of operator algebras I.
- Towards a quantum domain theory: order-enrichment and fixpoints in W^*-algebras
- Towards a quantum programming language
Cited in
(14)- Semantics of quantum programming languages: Classical control, quantum control
- Semantics for first-order affine inductive data types via slice categories
- LNL-FPC: the linear/non-linear fixpoint calculus
- Complexity of Grammar Induction for Quantum Types
- Computational adequacy for substructural lambda calculi
- scientific article; zbMATH DE number 7453968 (Why is no real title available?)
- Classical control, quantum circuits and linear logic in enriched category theory
- A computer scientist’s reconstruction of quantum theory*
- Type-safe quantum programming in Idris
- Semantics for a lambda calculus for string diagrams
- Quantum CPOs
- Quantum expectation transformers for cost analysis
- Combining quantum and classical control: syntax, semantics and adequacy
- Categories of quantum cpos
This page was built for publication: Quantum programming with inductive datatypes: causality and affine type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2200848)
