The dagger lambda calculus
From MaRDI portal
Publication:4997293
zbMATH Open1464.03008arXiv1406.1633MaRDI QIDQ4997293FDOQ4997293
Authors: Philip Atzemoglou 
Publication date: 29 June 2021
Abstract: We present a novel lambda calculus that casts the categorical approach to the study of quantum protocols into the rich and well established tradition of type theory. Our construction extends the linear typed lambda calculus with a linear negation of "trivialised" De Morgan duality. Reduction is realised through explicit substitution, based on a symmetric notion of binding of global scope, with rules acting on the entire typing judgement instead of on a specific subterm. Proofs of subject reduction, confluence, strong normalisation and consistency are provided, and the language is shown to be an internal language for dagger compact categories.
Full work available at URL: https://arxiv.org/abs/1406.1633
Recommendations
- Dagger compact closed categories and completely positive maps (extended abstract)
- A categorical quantum logic
- Strong normalization theorems for quantized \(\lambda \)-calculi
- On a measurement-free quantum lambda calculus with classical control
- A double effect \(\lambda \)-calculus for quantum computation
Quantum computation (81P68) Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Dagger categories, categorical quantum mechanics (18M40)
Cited In (3)
This page was built for publication: The dagger lambda calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4997293)
