Journal article
Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages
Abstract
The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms. We establish a correspondence between the …
Authors
Choudhury V; Karwowski J; Sabry A
Journal
Proceedings of the ACM on Programming Languages, Vol. 6, No. POPL, pp. 1–32
Publisher
Association for Computing Machinery (ACM)
Publication Date
January 16, 2022
DOI
10.1145/3498667
ISSN
2475-1421