| Definition of Random Sequences | 1966 |
| Algorithms and randomness | 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 | 1971 |
| Complexity Oscillations in Infinite Binary Sequences | 1971 |
| Infinite terms and a system of natural deduction | 1972 |
| An Intuitionistic Theory of Types | 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 | 1974 |
| An Intuitionistic Theory of Types: Predicative Part (Proceedings of the logic colloquium Bristol, July 1973) | 1975 |
| About Models for Intuitionistic Type Theories and the notion of Definitional Equality | 1975 |
| Syntax and semantics of the language of primitive recursive functions (Preprint written with Peter Hancock) | 1975 |
| Reply to Sverdrups Polemical Article Tests without Power | 1975 |
| A note to Michael Dummett | 1976 |
| Exact tests, confidence regions and estimates | 1977 |
| Constructive mathematics and computer programming (Tech report) | 1979 |
| Constructive mathematics and computer programming (Version 2) (Tech report) | 1979 |
| Constructive mathematics and computer programming | 1982 |
| On the Meanings of the Logical Constants and the Justification of Logical Laws | 1983 |
| Notes on The Domain Interpretation of Type Theory | 1983 |
| Intuitionistic Type Theory (Bibliopolis Book, notes by Giovanni Sambin of a series of lectures given in Padua, June 1980) (Re-typeset and searchable version) | 1984 |
| The logic of Judgements | 1987 |
| The logic of Judgements (typeset) | 1987 |
| Truth of a Proposition, Evidence of a Judgment, Validity of a Proof | 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 | 1990 |
| A path from logic to metaphysics (typescript) | 1990 |
| A path from logic to metaphysics | 1991 |
| Substitution calculus (Notes from a lecture given in Göteborg) | 1992 |
| Philosophical aspects of intuitionistic type theory* (Series of talks given at Leiden, 23 September – 16 December 1993) | 1993 |
| Analytic and Synthetic Judgements in Type Theory | 1994 |
| Truth and Knowability: On the Principles C and K of Michael Dummett | 1998 |
| The sense/reference distinction in constructive semantics* (The Bulletin of Symbolic Logic, 27, 501-513, 2021) | 2001 |
| Husserl's correlation between formal logic and formal ontology* (Talks given at Bern, 17 January) | 2002 |
| Are the objects of propositional attitudes propositions in the sense of propositional and predicate logic? | 2003 |
| Are the objects of propositional attitudes propositions in the sense of propositional and predicate logic?* (Talks given at Geneva, 19 December) | 2003 |
| Sets, types and categories* (Talks given at Leiden, 6 February) | 2004 |
| Normalization by Evaluation and by the Method of Computability (Talk at JAIST, Kanazawa) | 2004 |
| Hilbert Brouwer Controversy Resolved? | 2008 |
| One hundred years of Zermelo's axiom of choice. What was the problem with it? | 2009 |
| How did 'judgement' come to be a term of logic?* (Talks given at Paris, 14 October) | 2011 |
| Verificationism Then and Now | 2013 |
| Truth of empirical propositions* (Talks given at Leiden, 4 February) | 2014 |
| Making sense of normalization by evaluation (Talk given at a workshop on Type theory and formalization of mathematics in Gothenburg, December 11th) | 2014 |
| Is logic part of normative ethics?* (Talks given at Paris, 15 May) | 2015 |
| The two interpretations of natural deduction: how do they fit together?* (Talks given at Tübingen, 28 November) | 2015 |
| Judgement and inference* (Talks given at Marseille, 1 June) | 2016 |
| Assertion and request* (Talks given at Stockholm, 14 August) | 2017 |
| Assertion and request* (Talks given at Oslo, 29 August) | 2017 |
| Weyl's attempted mediation between intuitionism and formalism* (Talks given at Leeds, 12 September) | 2018 |
| Epistemic assumptions: are they assumed to be backwards vindicated or forwards vindicable?* (Leiden, 6 September) | 2019 |
| Logic and ethics* (Logica Yearbook 2019, I. Sedlár and M. Blicha (eds.). London: College Publications, 2020) | 2020 |
| Correctness of assertion and validity of inference* (Stockholm, 26 October) | 2022 |