An intuitionistic theory of types. Martin-Löf, P. In Twenty-five years of constructive type theory (Venice, 1995), volume 36, of Oxford Logic Guides, pages 127–172. Oxford Univ. Press, New York, 1998. ZSCC: 0000299 Citation Key Alias: martin-lof1998![An intuitionistic theory of types [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper abstract bibtex An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis.
@incollection{martin-lof_intuitionistic_1998,
series = {Oxford {Logic} {Guides}},
title = {An intuitionistic theory of types},
volume = {36},
url = {https://mathscinet.ams.org/mathscinet-getitem?mr=1686864},
abstract = {An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis.},
booktitle = {Twenty-five years of constructive type theory ({Venice}, 1995)},
publisher = {Oxford Univ. Press, New York},
author = {Martin-Löf, Per},
year = {1998},
mrnumber = {1686864},
note = {ZSCC: 0000299
Citation Key Alias: martin-lof1998},
pages = {127--172}
}
Downloads: 0
{"_id":"eg7vE54goTKWkR2Zt","bibbaseid":"martinlf-anintuitionistictheoryoftypes-1998","authorIDs":[],"author_short":["Martin-Löf, P."],"bibdata":{"bibtype":"incollection","type":"incollection","series":"Oxford Logic Guides","title":"An intuitionistic theory of types","volume":"36","url":"https://mathscinet.ams.org/mathscinet-getitem?mr=1686864","abstract":"An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis.","booktitle":"Twenty-five years of constructive type theory (Venice, 1995)","publisher":"Oxford Univ. Press, New York","author":[{"propositions":[],"lastnames":["Martin-Löf"],"firstnames":["Per"],"suffixes":[]}],"year":"1998","mrnumber":"1686864","note":"ZSCC: 0000299 Citation Key Alias: martin-lof1998","pages":"127–172","bibtex":"@incollection{martin-lof_intuitionistic_1998,\n\tseries = {Oxford {Logic} {Guides}},\n\ttitle = {An intuitionistic theory of types},\n\tvolume = {36},\n\turl = {https://mathscinet.ams.org/mathscinet-getitem?mr=1686864},\n\tabstract = {An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis.},\n\tbooktitle = {Twenty-five years of constructive type theory ({Venice}, 1995)},\n\tpublisher = {Oxford Univ. Press, New York},\n\tauthor = {Martin-Löf, Per},\n\tyear = {1998},\n\tmrnumber = {1686864},\n\tnote = {ZSCC: 0000299 \nCitation Key Alias: martin-lof1998},\n\tpages = {127--172}\n}\n\n","author_short":["Martin-Löf, P."],"key":"martin-lof_intuitionistic_1998","id":"martin-lof_intuitionistic_1998","bibbaseid":"martinlf-anintuitionistictheoryoftypes-1998","role":"author","urls":{"Paper":"https://mathscinet.ams.org/mathscinet-getitem?mr=1686864"},"downloads":0},"bibtype":"incollection","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.812Z","downloads":0,"keywords":[],"search_terms":["intuitionistic","theory","types","martin-löf"],"title":"An intuitionistic theory of types","year":1998,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}