## The collected works of Per Martin-Löf

Please inform us of any inaccuracies or missing works.

| Title | Date |
|:------|:----:|
|[Definition of Random Sequences](http://archive-pml.github.io/martin-lof/pdfs/Definition-of-Random-Sequences-1966.pdf)| 1966 |
|[Algorithms and randomness](http://archive-pml.github.io/martin-lof/pdfs/Algorithms-and-randomness-1969.pdf) | 1969 |
|Notes on constructive mathematics (Almqvist & Wiksell)| 1970 |
|A theory of types (Preprint, Stockholm University)| 1971 |
|[Hauptsatz for the intuitionistic theory of iterated inductive definitions](http://archive-pml.github.io/martin-lof/pdfs/Hauptsatz-for-the-intuitionistic-theory-of-iterated-inductive-definitions-1971.pdf)| 1971 |
|[Complexity Oscillations in Infinite Binary Sequences](http://archive-pml.github.io/martin-lof/pdfs/Complexity-Oscillations-in-Infinite-Binary-Sequences-1971.pdf) | 1971 |
|[Infinite terms and a system of natural deduction](http://archive-pml.github.io/martin-lof/pdfs/Infinite-terms-and-a-system-of-natural-deduction-1972.pdf)| 1972 |
|[An Intuitionistic Theory of Types](http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-1972.pdf)| 1972 |
|[The Notion of Redundancy and Its Use as a Quantitative Measure of the Discrepancy between a Statistical Hypothesis and a Set of Observational Data](http://archive-pml.github.io/martin-lof/pdfs/The-Notion-of-Redundancy-1974.pdf) | 1974 |
|[An Intuitionistic Theory of Types: Predicative Part](http://archive-pml.github.io/martin-lof/pdfs/An-Intuitionistic-Theory-of-Types-Predicative-Part-1975.pdf) (Proceedings of the logic colloquium Bristol, July 1973) | 1975 |
|[About Models for Intuitionistic Type Theories and the notion of Definitional Equality](http://archive-pml.github.io/martin-lof/pdfs/About-Models-for-Intuitionistic-Type-Theories-and-the-notion-of-Definitional-Equality-1975.pdf)| 1975 |
|[Syntax and semantics of the language of primitive recursive functions](http://archive-pml.github.io/martin-lof/pdfs/Syntax-and-semantics-of-the-language-of-primitive-recursive-functions-1975.pdf) (Preprint written with Peter Hancock)| 1975 |
|[Reply to Sverdrups Polemical Article Tests without Power](http://archive-pml.github.io/martin-lof/pdfs/Reply-to-Sverdrups-Polemical-Article-Tests-without-Power-1975.pdf)| 1975 |
|[A note to Michael Dummett](http://archive-pml.github.io/martin-lof/pdfs/Note-to-Michael-Dummett-1976.pdf)| 1976 |
|[Exact tests, confidence regions and estimates](http://archive-pml.github.io/martin-lof/pdfs/Exact-tests-confidence-regions-and-estimates-1977.pdf) | 1977 |
|[Constructive mathematics and computer programming](http://archive-pml.github.io/martin-lof/pdfs/Constructive-mathematics-and-computer-programming-1979.pdf) (Tech report)| 1979 |
|[Constructive mathematics and computer programming](http://archive-pml.github.io/martin-lof/pdfs/Constructive-mathematics-and-computer-programming-1982.pdf)| 1982 |
|[On the Meanings of the Logical Constants and the Justification of Logical Laws](http://archive-pml.github.io/martin-lof/pdfs/Meanings-of-the-Logical-Constants-1983.pdf)| 1983 |
|[Notes on The Domain Interpretation of Type Theory](http://archive-pml.github.io/martin-lof/pdfs/Notes-on-The-Domain-Interpretation-of-Type-Theory-1983.pdf)| 1983 |
|[Intuitionistic Type Theory](http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-1984.pdf) (Bibliopolis Book, notes by Giovanni Sambin of a series of lectures given in Padua, June 1980) [(Re-typeset and searchable version)](http://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf)| 1984 |
|[The logic of Judgements](http://archive-pml.github.io/martin-lof/pdfs/The-logic-of-judgements-1987.pdf) | 1987 |
|[Truth of a Proposition, Evidence of a Judgment, Validity of a Proof](http://archive-pml.github.io/martin-lof/pdfs/Truth-of-a-Proposition-Evidence-of-a-Judgment-1987.pdf)| 1987 |
|Philosophical implications of type theory (Lectures given at the Facoltà di Lettere e Filosofia, Universitá degli Studi di Firenze, Florence, March 15th - May 15th, Privately circulated notes)| 1987 |
|[Mathematics of Infinity](http://archive-pml.github.io/martin-lof/pdfs/Mathematics-of-Infinity.pdf)| 1990 |
|[A path from logic to metaphysics (typescript)](http://archive-pml.github.io/martin-lof/pdfs/A-path-from-logic-to-metaphysics-1990.pdf) | 1990 |
|[A path from logic to metaphysics](http://archive-pml.github.io/martin-lof/pdfs/A-path-from-logic-to-metaphysics-1991.pdf) | 1991 |
|[Substitution calculus](http://archive-pml.github.io/martin-lof/pdfs/Substitution-calculus-1992.pdf) (Notes from a lecture given in Göteborg)| 1992 |
|[Analytic and Synthetic Judgements in Type Theory](http://archive-pml.github.io/martin-lof/pdfs/Martin-Lof-Analytic-and-Synthetic-Judgements-in-Type-Theory.pdf)| 1994 |
|[Truth and Knowability: On the Principles C and K of Michael Dummett](http://archive-pml.github.io/martin-lof/pdfs/Truth-and-Knowability-On-the-Principles-C-and-K-of-Michael-Dummett-1998.pdf)| 1998 |
|[Hilbert Brouwer Controversy Resolved?](http://archive-pml.github.io/martin-lof/pdfs/Hilbert-Brouwer-Controversy-Resolved-2008.pdf)| 2008 |
|[Are the objects of propositional attitudes propositions in the sense of propositional and predicate logic?](http://archive-pml.github.io/martin-lof/pdfs/Are-the-objects-of-propositional-attitudes-propositions-in-the-sense-of-propositional-and-predicate-logic-2003.pdf) | 2003 |
|Normalization by Evaluation and by the Method of Computability (Talk at JAIST, Kanazawa) | 2004 |
|[One hundred years of Zermelo's axiom of choice. What was the problem with it?](http://archive-pml.github.io/martin-lof/pdfs/One-hundred-years-of-Zermelo-s-axiom-of-choice-what-was-the-problem-with-it-2009.pdf)| 2009 |
|[Verificationism Then and Now](http://archive-pml.github.io/martin-lof/pdfs/Martin-Lof-Verificationism-Then-and-Now-2013.pdf)| 2013 |
|[Making sense of normalization by evaluation](http://wiki.portal.chalmers.se/cse/pmwiki.php/ProgLog/TypeTheoryAndFormalizationOfMathematics) (Talk given at a workshop on Type theory and formalization of mathematics in Gothenburg, December 11th) | 2014 |