Teoria de tipus intuicionista
La teoria de tipus intuïcionista, en anglès: Intuitionistic type theory (també coneguda com a constructive type theory, o Martin-Löf type theory) és una teoria de tipus i un fonament matemàtic alternatiu basada en els principis del constructivisme matemàtic. Aquesta teoria va ser presentada pel matemàtic suec Per Martin-Löf el 1972. Martin-Löf l'ha modificada unes poques vegades, la seva formulació impredicativa de l'any 1971 era inconsistent com va demostrar la Paradoxa de Girard. Formulacions posteriors si eren predicatives.
La teoria de tipus intuïcionista està basada en certes analogies o isomorfismes entre proposicions i tipus.
Aquesta teoria internalitza la interpretació de la lògica intuicionista proposada per Brouwer, Heyting i Kolmogórov, l'anomenada com BHK interpretation.
Bibliografia
- Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programming in Martin-Löf's Type Theory. Oxford University Press. The book is out of print, but a free version can be picked up from here.
- Thompson, Simon (1991). Type Theory and Functional Programming Addison-Wesley. ISBN 0-201-41667-0.
- Granström, Johan G. (2011). Treatise on Intuitionistic Type Theory Springer. ISBN 978-94-007-1735-0.
Enllaços externs
- EU Types Project: Tutorials - lecture notes and slides from the Types Summer School 2005
- n-Categories - Sketch of a Definition - letter from John Baez and James Dolan to Ross Street, November 29, 1995
