Automath (automating mathematics) is 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.

PropertyValue
dbpprop:abstract
  • Automath (automating mathematics) is 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 represents as sets (called "categories") of their proofs, and the question of provability became a question of non-emptiness; de Brujin was unaware of Howard's work, and stated the correspondence independently. Automath was never widely publicized at the time, however, and so never achieved widespread use; nonetheless, it proved very influential in the development of later logical frameworks and proof assistants.
dbpprop:otheruses4Property
  • Autodidacticism
  • self-taught individuals
  • the programming language
dbpprop:reference
dbpprop:wikiPageUsesTemplate
rdfs:comment
  • Automath (automating mathematics) is 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.
rdfs:label
  • Automath
skos:subject
foaf:page
is dbpprop:redirect of