2026-07-24T03:16:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17474 2024-03-06T11:00:04Z ddc:004 open_access

A Curry-Howard Correspondence for Linear, Reversible Computation Chardonnet, Kostia Saurin, Alexis Valiron, Benoît Reversible Computation Linear Logic Curry-Howard In this paper, we present a linear and reversible programming language with inductives types and recursion. The semantics of the languages is based on pattern-matching; we show how ensuring syntactical exhaustivity and non-overlapping of clauses is enough to ensure reversibility. The language allows to represent any Primitive Recursive Function. We then give a Curry-Howard correspondence with the logic μMALL: linear logic extended with least fixed points allowing inductive statements. The critical part of our work is to show how primitive recursion yields circular proofs that satisfy μMALL validity criterion and how the language simulates the cut-elimination procedure of μMALL. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kostia Chardonnet and Alexis Saurin and Benoît Valiron 2023 Is Part Of LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2023.13 urn:nbn:de:0030-drops-174747 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.13 eng https://creativecommons.org/licenses/by/4.0/legalcode