A new implementation of Automath

DOI10.1023/A:1021983302516MaRDI QIDQ1868514zbMATH OpenFDO

Authors Freek Wiedijk

Publication date 27 April 2003

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/A:1021983302516

zbMATH Keywords

Automathformalized mathematicsproof objectstype theory

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• scientific article; zbMATH DE number 65527
• Verified representations of Landau's ``Grundlagen in the \(\lambda\delta\) family and in the calculus of constructions
• scientific article; zbMATH DE number 4058907
• Automath and Pure Type Systems

Cited in

(6)

• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Automath
• Characteristics of de Bruijn’s early proof checker Automath
• Verified representations of Landau's ``Grundlagen in the \(\lambda\delta\) family and in the calculus of constructions
• N. G. de Bruijn's contribution to the formalization of mathematics
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics

Describes a project that uses

Uses Software

• Coq
• Agda

This page was built for publication: A new implementation of Automath

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