摘要：在无穷lambda演算中，我们提出了一种新的、正式的共归证明Bohm规约的可合流性和规范化。该证明比以前的证明更简单。该证明的技术是新的，即它不仅仅是以前证明的共归改写。我们在Coq证明助手中对证明进行了形式化处理。
作者：{L}ukasz Czajka
论文ID：1808.05481
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22
PDF 下载： 英文版 中文版pdf翻译中