The Formalization of two Computational Models in Dafny

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

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…