This article is about the programming language. For self-taught individuals, see Autodidacticism.
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 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.[1]
L. S. van Benthem Jutting, as part of this Ph.D. thesis in 1976, translated Edmund Landau's Foundations of Analysis into Automath and checked its correctness.
Automath was never widely publicized at the time, however, and so never achieved widespread use; nonetheless, it proved very influential in the later development of logical frameworks and proof assistants.[2][3] The Mizar system, a system of writing and checking formalized mathematics that is still in active use, was influenced by Automath.
^Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry–Howard isomorphism, Elsevier, 2006, ISBN0-444-52077-5, pp 98-99
^R. P. Nederpelt, J. H. Geuvers, R. C. de Vrijer (1994) Selected Papers on Automath. Vol. 133 of Studies Logic, Elsevier, Amsterdam. ISBN0-444-89822-0.
^F. Kamareddine (2003) Thirty-five years of automating mathematics. Workshop, Dordrecht, Boston, published by Kluwer Academic Publishers, ISBN1-4020-1656-5.
External linksedit
The Automath Archive (mirror)
Thirty Five years of Automath homepage of a workshop to celebrate the 35th year of Automath
Automath page by Freek Wiedijk
This formal methods-related article is a stub. You can help Wikipedia by expanding it.
automath, this, article, about, programming, language, self, taught, individuals, autodidacticism, automating, mathematics, formal, language, devised, nicolaas, govert, bruijn, starting, 1967, expressing, complete, mathematical, theories, such, that, included,. This article is about the programming language For self taught individuals see Autodidacticism 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 Contents 1 Overview 2 See also 3 References 4 External linksOverview editThe 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 1 L S van Benthem Jutting as part of this Ph D thesis in 1976 translated Edmund Landau s Foundations of Analysis into Automath and checked its correctness Automath was never widely publicized at the time however and so never achieved widespread use nonetheless it proved very influential in the later development of logical frameworks and proof assistants 2 3 The Mizar system a system of writing and checking formalized mathematics that is still in active use was influenced by Automath See also editQED manifestoReferences edit Morten Heine Sorensen Pawel Urzyczyn Lectures on the Curry Howard isomorphism Elsevier 2006 ISBN 0 444 52077 5 pp 98 99 R P Nederpelt J H Geuvers R C de Vrijer 1994 Selected Papers on Automath Vol 133 of Studies Logic Elsevier Amsterdam ISBN 0 444 89822 0 F Kamareddine 2003 Thirty five years of automating mathematics Workshop Dordrecht Boston published by Kluwer Academic Publishers ISBN 1 4020 1656 5 External links editThe Automath Archive mirror Thirty Five years of Automath homepage of a workshop to celebrate the 35th year of Automath Automath page by Freek Wiedijk nbsp This formal methods related article is a stub You can help Wikipedia by expanding it vte Retrieved from https en wikipedia org w index php title Automath amp oldid 1012881939, wikipedia, wiki, book, books, library,
