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 the type formation-rules:

  • 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 January 3, 2023 at 00:20:06. See the history of this page for a list of all contributions to it.