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
- scientific article; zbMATH DE number 7350775 (Why is no real title available?)
- 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
- Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
- Quantum Entanglement Analysis Based on Abstract Interpretation
- Quantum Programs as Kleisli Maps
- Quantum collections
- Quantum programming languages: survey and bibliography
- 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
(12)- Semantics for first-order affine inductive data types via slice categories
- Semantics of quantum programming languages: Classical control, quantum control
- Classical control, quantum circuits and linear logic in enriched category theory
- A computer scientist’s reconstruction of quantum theory*
- Semantics for a lambda calculus for string diagrams
- scientific article; zbMATH DE number 7350775 (Why is no real title available?)
- scientific article; zbMATH DE number 7454912 (Why is no real title available?)
- scientific article; zbMATH DE number 7453968 (Why is no real title available?)
- Quantum CPOs
- Quantum expectation transformers for cost analysis
- Type-safe quantum programming in Idris
- Complexity of Grammar Induction for Quantum Types
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)
