University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Symmetries in Reversible Programming

Symmetries in Reversible Programming

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

  • UserVikraman Choudhury, University of Indiana
  • ClockFriday 27 May 2022, 14:00-15:00
  • HouseSS03.

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity