Intuitionistic Type Theory

by Per Martin-Löf

Genres: Mathematics, Logic, Nonfiction, Textbooks, Computer Science

91 pages, Paperback

First published January 1, 1985

Reviews

[Ian · Rating 4 out of 5]

I’d highly recommend reading “Truth of a Proposition, Evidence of a judgement, Validity of a Proof” prior to attempting to tackle these notes if you are less familiar with the context under which this formal system is being developed. At my first cut, much of the initial development seemed arbitrary and unclear. I think the lighter paper does a reasonable job of placing intuitionistic type theory in context of earlier work that was presumably assumed of the audience for these lecture notes

[Didier "Dirac Ghost" Gaulin · Rating 4 out of 5]

A text which contains the essential insights of Per Martin-Lof type theory, critical for any theoretical computer scientists and mathematicians with an eye on proof/model theory.