Automath is a programming language created in 1967 by Nicolaas Govert de Bruijn.
| #1852on PLDB | 59Years Old |
Automath is a formal language and theorem prover for expressing and verifying complete mathematical theories, developed by Nicolaas Govert de Bruijn starting in 1967. It was the first practical system to exploit the Curry-Howard correspondence and introduced concepts like dependent types and typed lambda calculus.