Soy consciente de que se hizo una pregunta similar sobre la teoría de tipos en los principia, pero estoy más interesado en cuál es la relación entre, digamos, la teoría de tipos de Martin-Lof y la lógica intuicionista.
Para la teoría de tipos puedes ver:
Peter Andrews, Introducción a la lógica matemática y la teoría de tipos: a la verdad a través de la prueba (1986)
J. Roger Hindley, Teoría básica de tipos simples (1997)
Fairouz Kamareddine y Twan Laan, Una perspectiva moderna sobre la teoría de tipos (2004)
tanto como :
Sobre el TT intuicionista :
Per Martin-Löf, Teoría de tipos intuicionista (1984)
Johan Georg Granström, Tratado sobre la teoría intuicionista de tipos (2011).
José Weissmann