Verified representations of Landau's ``Grundlagen in the family and in the calculus of constructions

DOI10.6092/ISSN.1972-5787/4716MaRDI QIDQ5195263zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• A new implementation of Automath
• Coquand's calculus of constructions: A mathematical foundation for a proof development system
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• scientific article; zbMATH DE number 4058907
• The formal system λδ

Cited in

(1)

• A new implementation of Automath

Describes a project that uses

Uses Software

• Automath
• Coq

This page was built for publication: Verified representations of Landau's ``Grundlagen in the \(\lambda\delta\) family and in the calculus of constructions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5195263)