N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
type: Item
instance of: scholarly article
title: N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
zbMATH Open document ID: 1257.01016
author: Francien Dechesne
author: Rob Nederpelt
published in: The Mathematical Intelligencer
publication date: 2013-02-15T00:00:00Z
Mathematics Subject Classification ID: 01A70
Mathematics Subject Classification ID: 01A60
Mathematics Subject Classification ID: 68-03
zbMATH DE Number: 6136583
describes a project that uses: Isabelle
describes a project that uses: ML
describes a project that uses: HOL
describes a project that uses: Coq
describes a project that uses: Automath
MaRDI profile type: Publication
full work available at URL: s00283-012-9324-x
OpenAlex ID: W2106831151
cites work: Proof-assistants using dependent type systems
cites work: Q4122841
cites work: Q5650683
cites work: Q4175528
cites work: Q4519579
cites work: Jaap Seidel, a friend
cites work: The calculus of constructions
cites work: Q5287513
cites work: A framework for defining logics
cites work: Thirty-five years of automating mathematics. Dedicated to 35 years of de Bruijn's Automath
cites work: Q5795193
cites work: N. G. de Bruijn's contribution to the formalization of mathematics
cites work: Q3999860
cites work: LCF considered as a programming language
cites work: Q3250680
cites work: Q5786798
cites work: The roots of trigonometric integrals
cites work: Q5797130
cites work: Q5804302
cites work: Q3251603
cites work: Q3254323
cites work: Q5686521
cites work: Q4087300
cites work: Q3905310
DOI: 10.1007/S00283-012-9324-X
description: scientific article; zbMATH DE number 6136583