Semantics of higher-order quantum computation via geometry of interaction
From MaRDI portal
Abstract: While much of the current study on quantum computation employs low-level formalisms such as quantum circuits, several high-level languages/calculi have been recently proposed aiming at structured quantum programming. The current work contributes to the semantical study of such languages by providing interaction-based semantics of a functional quantum programming language; the latter is, much like Selinger and Valiron's, based on linear lambda calculus and equipped with features like the ! modality and recursion. The proposed denotational model is the first one that supports the full features of a quantum functional programming language; we prove adequacy of our semantics. The construction of our model is by a series of existing techniques taken from the semantics of classical computation as well as from process theory. The most notable among them is Girard's Geometry of Interaction (GoI), categorically formulated by Abramsky, Haghverdi and Scott. The mathematical genericity of these techniques---largely due to their categorical formulation---is exploited for our move from classical to quantum.
Recommendations
- Applying quantitative semantics to higher-order quantum computing
- The geometry of parallelism: classical, probabilistic, and quantum effects
- Semantics for a quantum programming language by operator algebras
- On a fully abstract model for a quantum linear functional language (extended abstract)
- Presheaf models of quantum computation: an outline
Cites work
- scientific article; zbMATH DE number 1579275 (Why is no real title available?)
- scientific article; zbMATH DE number 1670816 (Why is no real title available?)
- scientific article; zbMATH DE number 1705158 (Why is no real title available?)
- scientific article; zbMATH DE number 2185654 (Why is no real title available?)
- scientific article; zbMATH DE number 5708038 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 3967883 (Why is no real title available?)
- scientific article; zbMATH DE number 4103051 (Why is no real title available?)
- scientific article; zbMATH DE number 4123722 (Why is no real title available?)
- scientific article; zbMATH DE number 2079022 (Why is no real title available?)
- A Lambda Calculus for Quantum Computation
- An axiomatic basis for computer programming
- An overview of QML with a concrete implementation in Haskell
- Applying quantitative semantics to higher-order quantum computing
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Categories for Types
- Category seminar. Proceedings Sydney category theory seminar 1972/1973
- Confluence results for a quantum lambda calculus with measurements
- Finiteness spaces
- From coalgebraic to monoidal traces
- Full abstraction for PCF
- Functorial Boxes in String Diagrams
- Game semantics for quantum stores
- Generic Trace Semantics via Coinduction
- Geometry of Interaction and linear combinatory algebras
- Geometry of synthesis III
- Geometry of synthesis. II: From games to delay-insensitive circuits
- Geometry of synthesis. IV: Compiling affine recursion into static hardware
- Linear Realizability
- Linear realizability and full completeness for typed lambda-calculi
- Linearly distributive functors
- Measurements in proof nets as higher-order quantum circuits
- Memoryful geometry of interaction: from coalgebraic components to algebraic effects
- Normal functors, power series and -calculus
- Notions of computation and monads
- On a fully abstract model for a quantum linear functional language (extended abstract)
- On full abstraction for PCF: I, II and III
- On multiplicative linear logic, modality and quantum circuits
- On the final sequence of a finitary set functor
- On traced monoidal closed categories
- PSEUDO-TELEPATHY: INPUT CARDINALITY AND BELL-TYPE INEQUALITIES
- Parallelism and synchronization in an infinitary context
- Probabilistic coherence spaces as a model of higher-order probabilistic computation
- Programming as a Discipline of Mathematical Nature
- Quantum alternation: prospects and problems
- Quantum computation: from a programmer's perspective
- Realizability. An introduction to its categorical side
- Relating computational effects by \(\top \top \)-lifting
- Reversible, irreversible and optimal \(\lambda\)-machines
- States of convex sets
- States, effects, and operations. Fundamental notions of quantum theory. Lectures in mathematical physics at the University of Texas at Austin. Ed. by A. Böhm, J. D. Dollard and W. H. Wootters
- Term Rewriting and Applications
- The Category-Theoretic Solution of Recursive Domain Equations
- The geometry of synchronization
- The geometry of tensor calculus. I
- The quantum IO monad
- Towards a quantum programming language
- Traced monoidal categories
- Traces for coalgebraic components
- Two applications of analytic functors
- Universal coalgebra: A theory of systems
- Wave-style token machines and quantum lambda calculi
- [top ][top ]-closed relations and admissibility
Cited in
(14)- Measurements in proof nets as higher-order quantum circuits
- QPCF: higher-order languages and quantum circuits
- Classical control, quantum circuits and linear logic in enriched category theory
- The game semantics of game theory
- The geometry of parallelism: classical, probabilistic, and quantum effects
- Semantics for a quantum programming language by operator algebras
- Quantum programming with inductive datatypes: causality and affine type theory
- Presheaf models of quantum computation: an outline
- Quantum computation: from a programmer's perspective
- Applying quantitative semantics to higher-order quantum computing
- scientific article; zbMATH DE number 7649898 (Why is no real title available?)
- A quantum game semantics for the measurement calculus
- Universal constructions for (co)relations: categories, monoidal categories, and props
- \textsc{qPCF}: a language for quantum circuit computations
This page was built for publication: Semantics of higher-order quantum computation via geometry of interaction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q345711)
