A Curry-Howard Correspondence for Linear, Reversible Computation

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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-10
Main Authors: Chardonnet, Kostia, Saurin, Alexis, Valiron, Benoît
Format: Article
Language:English
Subjects:
Pattern matching
Programming languages
Recursive functions
Semantics
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 \(\mu\)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 \(\mu\)MALL validity criterion and how the language simulates the cut-elimination procedure of \(\mu\)MALL.
ISSN:2331-8422
DOI:10.48550/arxiv.2302.11887