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.

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