Fri 21 Jan 2022 13:30 - 13:55 at Salon III - Semantics 2 Chair(s): Marco Gaboardi

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic datatypes. In this paper, we give a denotational semantics for this language, using the language of weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of reversible circuits.

We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, establishing full abstraction and adequacy. We extend the already established Curry-Howard correspondence for Pi to a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and permutations. Our proof uses techniques from the theory of group presentations and rewriting systems to solve the word problem for symmetric groups.

Using the formalisation of our results, we show how to perform normalisation-by-evaluation, verification, and synthesis of reversible logic gates, motivated by examples from quantum computing.

Fri 21 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:45
Semantics 2POPL at Salon III
Chair(s): Marco Gaboardi Boston University
13:30
25m
Research paper
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming LanguagesInPerson
POPL
Vikraman Choudhury Indiana University; University of Cambridge, Jacek Karwowski University of Warsaw, Amr Sabry Indiana University
Link to publication DOI Media Attached
13:55
25m
Research paper
A Relational Theory of Effects and CoeffectsRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached
14:20
25m
Research paper
Effectful Program DistancingRemote
POPL
Ugo Dal Lago University of Bologna; Inria, Francesco Gavazzo University of Bologna; Inria
DOI Media Attached