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.

@article{paperbot3398,
  title = {A Curry-Howard Correspondence for Linear, Reversible Computation},
  author = {Kostia Chardonnet and Alexis Saurin and Benoît Valiron},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 3},
  year = {2025},
  doi = {10.46298/lmcs-21(3:4)2025}
}