| Publication | Date of Publication | Type |
|---|
Characteristics of de Bruijn’s early proof checker Automath Fundamenta Informaticae | 2022-07-14 | Paper |
Characteristics of de Bruijn's early proof checker Automath (available as arXiv preprint) | 2022-03-02 | Paper |
| Type theory and formal proof. An introduction | 2014-10-22 | Paper |
N. G. de Bruijn's contribution to the formalization of mathematics Indagationes Mathematicae. New Series | 2014-09-03 | Paper |
Automath and Pure Type Systems Electronic Notes in Theoretical Computer Science | 2013-06-06 | Paper |
N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker The Mathematical Intelligencer | 2013-02-15 | Paper |
Rewriting Techniques and Applications Lecture Notes in Computer Science | 2009-04-30 | Paper |
| Logical reasoning. A first course | 2006-03-27 | Paper |
Mathematical Knowledge Management Lecture Notes in Computer Science | 2005-08-26 | Paper |
| scientific article; zbMATH DE number 2154395 (Why is no real title available?) | 2005-04-09 | Paper |
A modern perspective on type theory. From its origins until today Applied Logic Series | 2004-11-25 | Paper |
A refinement of de Bruijn's formal language of mathematics Journal of Logic, Language and Information | 2004-08-16 | Paper |
| scientific article; zbMATH DE number 2086242 (Why is no real title available?) | 2004-08-11 | Paper |
Formalizing Belief Revision in Type Theory Logic Journal of the IGPL | 2003-07-16 | Paper |
Revisiting the notion of function The Journal of Logic and Algebraic Programming | 2003-06-25 | Paper |
Types in Logic and Mathematics before 1940 The Bulletin of Symbolic Logic | 2003-03-06 | Paper |
| scientific article; zbMATH DE number 1692907 (Why is no real title available?) | 2002-01-21 | Paper |
On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations Annals of Pure and Applied Logic | 2000-02-15 | Paper |
Dijkstra-Scholten predicate calculus: Concepts and misconceptions Acta Informatica | 1999-06-13 | Paper |
A useful \(\lambda\)-notation Theoretical Computer Science | 1997-09-09 | Paper |
A unified approach to type theory through a refined \(\lambda\)-calculus Theoretical Computer Science | 1997-02-27 | Paper |
A modern elaboration of the ramified theory of types Studia Logica | 1997-01-16 | Paper |
Canonical typing and ∏-conversion in the Barendregt Cube Journal of Functional Programming | 1996-11-17 | Paper |
The Barendregt cube with definitions and generalised reduction Information and Computation | 1996-07-03 | Paper |
Refining reduction in the lambda calculus Journal of Functional Programming | 1996-06-05 | Paper |
ON STEPWISE EXPLICIT SUBSTITUTION International Journal of Foundations of Computer Science | 1994-04-27 | Paper |