Journal of Formalized Reasoning (Jan 2012)

Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover

  • Ferruccio Guidi

Journal volume & issue
Vol. 5, no. 1
pp. 1 – 25

Abstract

Read online

We present a formalization of pure lambda-calculus for the Matita interactive theorem prover, including the proofs of two relevant results in reduction theory: the confluence theorem and the standardization theorem. The proof of the latter is based on a new approach recently introduced by Xi and refined by Kashima that, avoiding the notion of development and having a neat inductive structure, is particularly suited for formalization in theorem provers.

Keywords