Semantics of higher-order quantum computation via geometry of interaction
From MaRDI portal
Publication:345711
DOI10.1016/J.APAL.2016.10.010zbMATH Open1422.68161arXiv1605.05079OpenAlexW2533990420MaRDI QIDQ345711FDOQ345711
Publication date: 2 December 2016
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1605.05079
programming languagecategorical semanticsquantum computationdenotational semanticsgeometry of interactionhigher-order computation
Quantum computation (81P68) Logic in computer science (03B70) Eilenberg-Moore and Kleisli constructions for monads (18C20) Categorical semantics of formal languages (18C50) Semantics in the theory of computing (68Q55)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The geometry of tensor calculus. I
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Reversible, irreversible and optimal \(\lambda\)-machines
- Universal coalgebra: A theory of systems
- On full abstraction for PCF: I, II and III
- Full abstraction for PCF
- The Category-Theoretic Solution of Recursive Domain Equations
- Categories for Types
- Towards a quantum programming language
- Generic Trace Semantics via Coinduction
- On the final sequence of a finitary set functor
- Notions of computation and monads
- 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
- Functorial Boxes in String Diagrams
- On traced monoidal closed categories
- Geometry of Interaction and linear combinatory algebras
- Traced monoidal categories
- Geometry of synthesis III
- An axiomatic basis for computer programming
- Traces for coalgebraic components
- Realizability. An introduction to its categorical side
- Programming as a Discipline of Mathematical Nature
- Normal functors, power series and \(\lambda\)-calculus
- Linearly distributive functors
- Category seminar. Proceedings Sydney category theory seminar 1972/1973
- Relating computational effects by \(\top \top \)-lifting
- An overview of QML with a concrete implementation in Haskell
- Confluence results for a quantum lambda calculus with measurements
- On a fully abstract model for a quantum linear functional language (extended abstract)
- From coalgebraic to monoidal traces
- States of Convex Sets
- Geometry of Synthesis II: From Games to Delay-Insensitive Circuits
- PSEUDO-TELEPATHY: INPUT CARDINALITY AND BELL-TYPE INEQUALITIES
- Linear Realizability
- [top ][top ]-closed relations and admissibility
- The geometry of synchronization
- Memoryful geometry of interaction
- Parallelism and Synchronization in an Infinitary Context
- A Lambda Calculus for Quantum Computation
- Quantum computation: from a programmer's perspective
- Geometry of synthesis iv
- Applying quantitative semantics to higher-order quantum computing
- Measurements in Proof Nets as Higher-Order Quantum Circuits
- Game Semantics for Quantum Stores
- Probabilistic coherence spaces as a model of higher-order probabilistic computation
- Linear realizability and full completeness for typed lambda-calculi
- Finiteness spaces
- Term Rewriting and Applications
- Two applications of analytic functors
Cited In (9)
- QPCF: higher-order languages and quantum circuits
- $$\mathsf {qPCF}$$ : A Language for Quantum Circuit Computations
- Universal Constructions for (Co)Relations: categories, monoidal categories, and props
- The game semantics of game theory
- Semantics for a quantum programming language by operator algebras
- Quantum programming with inductive datatypes: causality and affine type theory
- Title not available (Why is that?)
- Quantum computation: from a programmer's perspective
- Title not available (Why is that?)
Uses Software
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)
