Characteristics of de Bruijn’s early proof checker Automath

DOI10.3233/FI-222112WikidataQ113701297 ScholiaQ113701297MaRDI QIDQ5089679

Rob Nederpelt, Herman Geuvers

Publication date: 14 July 2022

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2203.01173

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Coq
• Isabelle/HOL
• HOL
• Automath
• Agda
• Lean

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Proof assistants: history, ideas and future
• The calculus of constructions
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A useful \(\lambda\)-notation
• Isabelle/HOL. A proof assistant for higher-order logic
• On the rules of suppositions in formal logic
• A new implementation of Automath
• The Lean 4 theorem prover and programming language
• Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs
• Type Theory and Formal Proof
• A Brief Overview of Mizar
• A Brief Overview of Agda – A Functional Language with Dependent Types

This page was built for publication: Characteristics of de Bruijn’s early proof checker Automath