Symmetries in Reversible Programming

Add to your list(s) Download to your calendar using vCal

• Vikraman Choudhury, University of Indiana
• Friday 27 May 2022, 14:00-15:00
• SS03.

If you have a question about this talk, please contact Jamie Vicary.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• SS03
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.