nLab Per Martin-Löf

Selected writings

A first type theoretic formulation of general inductive definitions (precusor notion of inductive types):

Introducing Martin-Löf dependent type theory:

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)):

  • 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:

A list of publication is kept here:

Transcripts of a number of lectures of a philosophical nature is kept here:

category: people

Last revised on May 18, 2023 at 04:50:13. See the history of this page for a list of all contributions to it.