A first type theoretic formulation of general inductive definitions (precusor notion of inductive types):
Introducing Martin-Löf dependent type theory:
Per Martin-Löf, A Theory of Types, unpublished note (1971) [pdf, pdf]
Per Martin-Löf, Section 1.7 in: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 Pages 73-118, Elsevier 1975 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)
Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) (pdf, pdf)
and regarded as a programming language:
and with emphasis on the meaning of judgements and type formation-rules (via the intuitionistic interpretation of connectiveslogic#ConstructiveInterpretationOfConnectives)):
On the notion of judgement:
On analytic versus synthetic judgements in type theory:
A list of publications:
Transcripts of a number of lectures of a philosophical nature is kept here:
Last revised on July 12, 2025 at 18:31:53. See the history of this page for a list of all contributions to it.