The dagger lambda calculus

Abstract

We present a novel lambda calculus that casts the categorical approach to the study of quantum protocols [4] into the rich and well established tradition of type theory. Our construction extends the linear typed lambda calculus [6] with a linear negation [1] of "trivialised" De Morgan duality [5]. 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.