发表机构
Alexandru Ioan Cuza University of Ia s i, Romania
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究在Dafny中完成图灵机与Lambda演算两种计算模型的形式化，并实现了图灵机终止性证明、丘奇编码证明及丘奇-罗瑟定理机械化证明等多项应用。
AI 中文摘要
我们描述了图灵机与Lambda演算这两种计算模型在Dafny中的形式化工作。我们展示了该形式化的若干应用：图灵机终止性的机器证明、丘奇编码的Dafny证明，以及丘奇-罗瑟定理的机械化证明。
英文摘要
We describe the formalization in Dafny of two computational models, Turing Machines and the Lambda Calculus. We present several application of the formalizations: machine proofs of termination for Turing machines, Dafny proofs for Church encodings, and a mechanized proof of the Church-Rosser theorem.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 82-91
