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.

翻译：本文提出了一种具有归纳类型和递归的线性可逆编程语言。该语言的语义基于模式匹配；我们证明了确保子句的语法穷尽性和无重叠性足以保证可逆性。该语言能够表示任何原始递归函数。随后，我们给出了与μMALL逻辑的Curry-Howard对应关系，该逻辑是线性逻辑扩展了允许归纳陈述的最小不动点。我们工作的关键部分在于展示原始递归如何生成满足μMALL有效性准则的循环证明，以及该语言如何模拟μMALL的消割过程。