Abstract

Reversible computing is a model of computation, motivated by physical principles, where computation happens in an information-preserving way. Reversible programs are usually expressed as reversible boolean functions, reversible boolean gates, or sequences of reversible operations on bits, which can be run forwards or backwards on a reversible computer.

Towards building a high-level calculus for reversible programming, Sabry and his collaborators formulated the Pi family of reversible programming languages, which are typed high-level languages for writing total reversible programs. In this talk, I will discuss the semantics foundations of this family of languages, using groupoids.

The Pi language has constructs for expressing reversible programs on finite number of bits, and their equivalences. The syntactic groupoid of this languages presents the free symmetric rig groupoid on zero generators, which is shown to be equivalent to the groupoid of finite sets and bijections. This leads to a fully-abstract and fully-complete denotational semantics for the language. The proof uses various tools and techniques from presentations of symmetric monoidal categories, coherence theorems, presentations of symmetric groups, permutation codes, and ideas from normalisation-by-evaluation in programming language theory.

Finally, there are some applications of this semantics to reversible boolean circuits, motivated by examples from quantum computing. I will show how to perform normalisation-by-evaluation, verification, and synthesis of reversible boolean gates, and how to reason about and transfer theorems between different representations of reversible circuits.