名称生成的证明相关逻辑关系
摘要：用证明相关的逻辑关系的新框架在直接风格下对具有递归的$u$-calculus类似语言进行了建模。在这种框架中，逻辑关系也包含了证明对象（或证明）来证明（语义上相当于）程序的等价性。除了为一个古老问题提供了一个新的解决方案外，这项工作还提供了一个可访问的环境，可以不涉及与更复杂语言的使用相关的额外复杂性，来介绍使用证明相关的逻辑关系的方法。
作者：Nick Benton, Martin Hofmann, Vivek Nigam
论文ID：1708.05193
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22