线性、可逆计算的Curry-Howard对应
摘要：线性可逆编程语言与归纳类型和递归一起呈现。语言的语义基于模式匹配；我们展示了如何确保句法的详尽性和不重叠的子句足以确保可逆性。该语言允许表示任何原始递归函数。然后，我们给出了与逻辑$mu$MALL的Curry-Howard对应：线性逻辑扩展了具有归纳陈述的最小不动点。我们工作的关键部分是展示原始递归如何产生满足$mu$MALL有效性准则的循环证明，以及语言如何模拟$mu$MALL的削减消除过程。
作者：Kostia Chardonnet, Alexis Saurin, Beno^it Valiron
论文ID：2302.11887
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-01