Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A Curry-Howard Correspondence for Linear, Reversible Computation

Kostia Chardonnet 1, 2 Alexis Saurin 1, 3 Benoît Valiron 2 
2 QuaCS - Quantum Computation Structures
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
3 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UPCité - Université Paris Cité, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
Abstract : 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 xed 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03747425
Contributor : Kostia Chardonnet Connect in order to contact the contributor
Submitted on : Monday, August 8, 2022 - 11:34:16 AM
Last modification on : Tuesday, September 6, 2022 - 1:27:10 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Kostia Chardonnet, Alexis Saurin, Benoît Valiron. A Curry-Howard Correspondence for Linear, Reversible Computation. 2022. ⟨hal-03747425⟩

Share

Metrics

Record views

31

Files downloads

13