一句话：提出线性可逆语言及其与 μMALL 的 Curry-Howard 对应，用原始递归生成满足有效性的循环证明并模拟切消。
本文研究线性且可逆的编程语言及其逻辑基础。作者定义了一种带归纳类型与递归的线性可逆语言，其操作语义基于模式匹配；通过要求模式子句语法上穷尽且互不重叠，保证求值可逆。该语言足以表示所有原始递归函数。随后，文章建立该语言与 μMALL（带最小不动点、支持归纳陈述的线性逻辑）之间的 Curry-Howard 对应。关键贡献在于说明原始递归如何产生满足 μMALL 有效性判据的循环证明，并展示语言如何模拟 μMALL 的切消过程，从而将可逆计算与线性逻辑证明论联系起来。
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 $μ$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 $μ$MALL validity criterion and how the language simulates the cut-elimination procedure of $μ$MALL.
@article{paperbot3398,
title = {A Curry-Howard Correspondence for Linear, Reversible Computation},
author = {Kostia Chardonnet and Alexis Saurin and Benoît Valiron},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:4)2025}
}