N. G. de Bruijn's contribution to the formalization of mathematics
From MaRDI portal
Publication:740481
DOI10.1016/J.INDAG.2013.09.003zbMath1359.03003OpenAlexW2151993589MaRDI QIDQ740481
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
Biographies, obituaries, personalia, bibliographies (01A70) Mechanization of proofs and logical operations (03B35) History of mathematical logic and foundations (03-03) Combinatory logic and lambda calculus (03B40)
Related Items (1)
Uses Software
Cites Work
- The lambda calculus. Its syntax and semantics. Rev. ed.
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- Edinburgh LCF. A mechanized logic of computation
- A new implementation of Automath
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
- Type Theory and Formal Proof
- Interacting with Modal Logics in the Coq Proof Assistant
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Simple Types in Type Theory: Deep and Shallow Encodings
- The Isabelle Framework
- Explicit substitutions
- Explicit substitutions with de bruijn's levels
- Mathematical Knowledge Management
- On Correctness of Mathematical Texts from a Logical and Practical Point of View
- Intensional interpretations of functionals of finite type I
- 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
- Unnamed Item
This page was built for publication: N. G. de Bruijn's contribution to the formalization of mathematics
