Formalizing computing models for machine verification and proofs

The Formalization of two Computational Models in Dafny

Mon 28 Sept 2026Logic in Computer ScienceFormal Languages and Automata TheoryProgramming Languages

Computers can be understood using simple models like Turing Machines and the Lambda Calculus, which explain how computations happen step-by-step. This paper shows how these models were precisely described using a programming language called Dafny. The formal descriptions help prove that certain machines always finish their work and verify important mathematical properties about functions. This helps ensure that computer systems behave correctly by checking their fundamental building blocks.

What this means in practice

For software verification engineers: Use formal models of computation to prove software components always finish and behave as expected.
For programming language designers: Employ formal proofs of lambda calculus properties to build more reliable and mathematically sound programming languages.

Authors

Ştefan Ciobâc\b{a}, Diana-Elena Gratie, Dragoş-Irinel Rotariu

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.

View PDFOpen arXiv

Formalizing computing models for machine verification and proofs

Summary

What this means in practice

Authors

Abstract