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 的咖哩- Howard对应词: 线性逻辑延伸至最不固定的点, 允许感应语句。 我们工作的关键部分是显示原始递归如何产生符合 {mu} malall 有效性标准的循环证明, 以及语言如何模拟 {mule mall 的切除程序 。