N. G. de Bruijn's contribution to the formalization of mathematics

DOI10.1016/j.indag.2013.09.003zbMath1359.03003MaRDI QIDQ740481

Herman Geuvers, Rob Nederpelt

Publication date: 3 September 2014

Published in: Indagationes Mathematicae. New Series (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.indag.2013.09.003

zbMATH Keywords

lambda calculus; type theory; proof assistants; formalizing mathematics

Mathematics Subject Classification ID

01A70: Biographies, obituaries, personalia, bibliographies

03B35: Mechanization of proofs and logical operations

03-03: History of mathematical logic and foundations

03B40: Combinatory logic and lambda calculus

Uses Software

• Coq
• Isabelle
• ML
• HOL
• Twelf
• Automath
• NQTHM
• LCF
• SAD