Abstract
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching and to interpret inductive types and recursion. We then derive a notion of completeness in the sense that any computable, partial, first-order injective function is the image of a term in the language.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction |
| Editors | Jakob Rehof |
| Place of Publication | Tallinn, Estonia |
| Publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
| Number of pages | 19 |
| ISBN (Electronic) | 9783959773232 |
| DOIs | |
| Publication status | Published - 5 Jul 2024 |
| Event | 9th International Conference on Formal Structures for Computation and Deduction - Tallinn University, Tallinn, Estonia Duration: 10 Jul 2024 → 13 Jul 2024 https://cs.ioc.ee/fscd24/index.html |
Publication series
| Name | Leibniz International Proceedings in Informatics |
|---|---|
| Publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
| Volume | 299 |
| ISSN (Electronic) | 1868-8969 |
Conference
| Conference | 9th International Conference on Formal Structures for Computation and Deduction |
|---|---|
| Abbreviated title | FSCD 2024 |
| Country/Territory | Estonia |
| City | Tallinn |
| Period | 10/07/24 → 13/07/24 |
| Internet address |
Keywords / Materials (for Non-textual outputs)
- reversible programming
- functional programming
- computability
- denotational semantics