Automath
Automath (automating mathematics) was a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness. The Automath system included many novel notions that were later adopted and/or reinvented in areas such as typed lambda calculus and explicit substitution. Dependent types is one outstanding example. Automath was also the first practical system that exploited the Curry–Howard correspondence. Propositions were represented as sets (called "categories") of their proofs, and the question of provability became a question of non-emptiness (type inhabitation); de Bruijn was unaware of Howard's work, and stated the correspondence independently.
influenced by
Wikipage redirect
primaryTopic
Automath
Automath (automating mathematics) was a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correctness. The Automath system included many novel notions that were later adopted and/or reinvented in areas such as typed lambda calculus and explicit substitution. Dependent types is one outstanding example. Automath was also the first practical system that exploited the Curry–Howard correspondence. Propositions were represented as sets (called "categories") of their proofs, and the question of provability became a question of non-emptiness (type inhabitation); de Bruijn was unaware of Howard's work, and stated the correspondence independently.
has abstract
Automath (automating mathemati ...... e, was influenced by Automath.
@en
Automath (geautomatiseerde wis ...... amwerken en bewijsassistenten.
@nl
Automath (pour « automating ma ...... assistants de preuve actuels.
@fr
Link from a Wikipage to an external page
Wikipage page ID
Wikipage revision ID
685.329.231
subject
type
comment
Automath (automating mathemati ...... correspondence independently.
@en
Automath (geautomatiseerde wis ...... Curry-Howard-correspondentie.
@nl
Automath (pour « automating ma ...... ait en vérifier la correction.
@fr
label
Automath
@en
Automath
@fr
Automath
@nl