The Formalization of two Computational Models in Dafny
arXiv:2609.34883 · doi:10.4204/EPTCS.452.6
Abstract
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.
In Proceedings FROM 2026, arXiv:2609.30324