A Curry-Howard Correspondence for Linear, Reversible Computation

Kostia Chardonnet, Alexis Saurin, Benoît Valiron

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…