Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions
Guidi, Ferruccio
Journal of Formalized Reasoning, Tome 9 (2016), / Harvested from Journal of Formalized Reasoning

Landau's "Grundlagen der Analysis" formalized in the language Aut-QE, represents an early milestone in computer-checked mathematics and is the only non-trivial development finalized in the languages of the Automath family. Here we discuss an implemented procedure producing a faithful representation of the Grundlagen in the Calculus of Constructions, verified by the proof assistant Coq 8.4.3. The point at issue is distinguishing lambda-abstractions from pi-abstractions where the original text uses Automath unified binders, taking care of the cases in which a binder corresponds to both abstractions at one time. It is a fact that some binders can be disambiguated only by verifying the Grundlagen in a calculus accepting Aut-QE and the Calculus of Constructions. To this end, we rely on lambda-delta version 3, a system that the author is proposing here for the first time.

Publié le : 2016-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/4716
@article{4716,
     title = {Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions},
     journal = {Journal of Formalized Reasoning},
     volume = {9},
     year = {2016},
     doi = {10.6092/issn.1972-5787/4716},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/4716}
}
Guidi, Ferruccio. Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions. Journal of Formalized Reasoning, Tome 9 (2016) . doi : 10.6092/issn.1972-5787/4716. http://gdmltest.u-ga.fr/item/4716/