Per Martin-Löf in nLab
Selected writings
A first type theoretic formulation of general inductive definitions (precusor notion of inductive types):
- Per Martin-Löf, Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions, Studies in Logic and the Foundations of Mathematics 63 (1971) 179-216 [doi:10.1016/S0049-237X(08)70847-4]
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:
- Per Martin-Löf, Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 [doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0]
and with emphasis on the meaning of judgements and type formation-rules (via the intuitionistic interpretation of connectiveslogic#ConstructiveInterpretationOfConnectives)):
- Per Martin-Löf, On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Nordic Journal of Philosophical Logic, 1 1 (1996) 11-60 [pdf, pdf]
On the notion of judgement:
- Per Martin-Löf, Truth of a proposition, evidence of a judgement, validity of a proof, Synthese 73 (1987) 407–420 [doi:10.1007/BF00484985, pdf]
A list of publication is kept here:
Transcripts of a number of lectures of a philosophical nature is kept here:
Last revised on May 18, 2023 at 04:50:13. See the history of this page for a list of all contributions to it.