The dagger lambda calculus

TL;DR

This paper introduces the dagger lambda calculus, a new type-theoretic framework that models quantum protocols categorically, extending linear lambda calculus with negation and symmetric binding, and proves key properties.

Contribution

It presents a novel lambda calculus that captures dagger compact categories, integrating categorical quantum mechanics into type theory with explicit substitution and global scope binding.

Findings

Proves subject reduction, confluence, and strong normalization.

Shows the calculus as an internal language for dagger compact categories.

Provides a foundation for formal reasoning in quantum protocols.

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.