A new implementation of Automath

DOI10.1023/A:1021983302516zbMath1064.68084MaRDI QIDQ1868514

Freek Wiedijk

Publication date: 27 April 2003

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

zbMATH Keywords

type theoryformalized mathematicsAutomathproof objects

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics ⋮ Characteristics of de Bruijn’s early proof checker Automath ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Automath

Uses Software

• Coq
• Agda