The dagger lambda calculus

zbMATH Open1464.03008arXiv1406.1633MaRDI QIDQ4997293

Author name not available (Why is that?)

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

Mathematics Subject Classification ID

No records found.

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)