Kostia Chardonnet (LMF, Université Paris Saclay. IRIF, Université de Paris.) |
Louis Lemonnier (LMF, Université Paris Saclay.) |
Benoît Valiron (LMF, CentraleSupélec, Université Paris Saclay) |
This paper is concerned with categorical structures for reversible computation. In particular, we focus on a typed, functional reversible language based on Theseus. We discuss how join inverse rig categories do not in general capture pattern-matching, the core construct Theseus uses to enforce reversibility. We then derive a categorical structure to add to join inverse rig categories in order to capture pattern-matching. We show how such a structure makes an adequate model for reversible pattern-matching. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.351.2 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |