2014/06/30 by Philip Atzemoglou
Computer Science · Mathematics · Physics and Astronomy · #cs.LO #cs.PL #math.CT #quant-ph
paper · pdf · doi:10.4204/eptcs.172.15
published as EPTCS 172, 2014, pp. 217-235 · In Proceedings QPL 2014, arXiv:1412.8102
arxiv created 2014/12/30 · arxiv updated 2014/12/31
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.