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有效性准则的循环证明，以及该语言如何模拟μMALL的消去过程。