Intuitionistic Type Theory
by Per Martin-Loef
1980
Number of pages: 57
Description:
Contents: Introductory remarks; Propositions and judgements; Explanations of the forms of judgement; Propositions; Rules of equality; Hypothetical judgements and substitution rules; Judgements with more than one assumption and contexts; Sets and categories; General remarks on the rules; Cartesian product of a family of sets; Definitional equality; Applications of the cartesian product; Disjoint union of a family of sets; Applications of the disjoint union; The axiom of choice; The notion of such that; Disjoint union of two sets; Propositional equality; Finite sets; Consistency; Natural numbers; Lists; Wellorderings; Universes.
Download or read it online for free here:
Download link
(670KB, PDF)
Download mirrors:
Mirror 1
Similar books
Homotopy Type Theoryby Peter Aczel, et al. - Institute for Advanced Study
The present work has its origins in our collective attempts to develop a new style of 'informal type theory' that can be read and understood by a human being, as a complement to a formal proof that can be checked by a machine.
(6355 views)
Introduction to Type Theoryby Herman Geuvers - Radboud University Nijmegen
The author gives an introductory overview of type theory for PhD students. He focuses on the use of type theory for compile-time checking of functional programs and on the use of types in proof assistants (theorem provers).
(8453 views)
Programming in Martin-Lof's Type Theory: An Introductionby Bengt Nordstrom, Kent Petersson, Jan M. Smith - Oxford University Press
This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, and monomorphic sets. Martin-Lof's type theory makes possible the expression of both specifications and programs within the same formalism.
(9071 views)
Type Theory and Functional Programmingby Simon Thompson - Addison-Wesley
The book is a course in type theory. It includes introduction to logic and functional programming, the type theory with many examples, the system from a mathematical perspective, and a number of important properties of the theory.
(11070 views)