Characteristics of de Bruijn’s early proof checker Automath
From MaRDI portal
Publication:5089679
DOI10.3233/FI-222112WikidataQ113701297 ScholiaQ113701297MaRDI QIDQ5089679FDOQ5089679
Authors: Herman Geuvers, Rob Nederpelt 
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
Cites Work
- A new implementation of Automath
- A Brief Overview of Mizar
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- On the rules of suppositions in formal logic
- The calculus of constructions
- Title not available (Why is that?)
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Title not available (Why is that?)
- Title not available (Why is that?)
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- Proof-assistants using dependent type systems
- Type theory and formal proof. An introduction
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Proof assistants: history, ideas and future
- A useful \(\lambda\)-notation
- The Lean 4 theorem prover and programming language
- Translations between Gentzen-Prawitz and Jaśkowski-Fitch natural deduction proofs
Uses Software
This page was built for publication: Characteristics of de Bruijn’s early proof checker Automath
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089679)
