Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions

DOI10.6092/issn.1972-5787/4716zbMath1451.68341OpenAlexW2228407435MaRDI QIDQ5195263

Ferruccio Guidi

Publication date: 18 September 2019

Full work available at URL: https://dblp.uni-trier.de/db/journals/jfrea/jfrea8.html#Guidi15

zbMATH Keywords

Automathpure type systemGrundlagen der Analysisunified binders

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to real functions (26-01) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq
• Automath

This page was built for publication: Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions