N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker

DOI10.1007/s00283-012-9324-xzbMath1257.01016OpenAlexW2106831151MaRDI QIDQ1935352

Francien Dechesne, Rob Nederpelt

Publication date: 15 February 2013

Published in: The Mathematical Intelligencer (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00283-012-9324-x

Mathematics Subject Classification ID

History of mathematics in the 20th century (01A60) Biographies, obituaries, personalia, bibliographies (01A70) History of computer science (68-03)

Related Items (2)

Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician ⋮ N. G. de Bruijn's contribution to the formalization of mathematics

Uses Software

• Coq
• Isabelle
• ML
• HOL
• Automath

Cites Work

• Thirty-five years of automating mathematics. Dedicated to 35 years of de Bruijn's Automath
• N. G. de Bruijn's contribution to the formalization of mathematics
• The calculus of constructions
• LCF considered as a programming language
• The roots of trigonometric integrals
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker