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

Authors

  • Ferruccio Guidi University of Bologna

DOI:

https://doi.org/10.6092/issn.1972-5787/3392

Abstract

We present a formalization of pure ?-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.

Downloads

Published

2012-12-30

How to Cite

Guidi, F. (2012). Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover. Journal of Formalized Reasoning, 5(1), 1–25. https://doi.org/10.6092/issn.1972-5787/3392

Issue

Section

Articles