2026-08-06T21:03:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20348 2024-07-05T06:20:34Z ddc:004 open_access

Semantics for a Turing-Complete Reversible Programming Language with Inductive Types Chardonnet, Kostia Lemonnier, Louis Valiron, Benoît Reversible programming functional programming Computability Denotational Semantics 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kostia Chardonnet and Louis Lemonnier and Benoît Valiron 2024 Is Part Of LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2024.19 urn:nbn:de:0030-drops-203487 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.19 eng https://creativecommons.org/licenses/by/4.0/legalcode