Zur Zeit existiert kein Lehrbuch, das die gesamte Thematik abdeckt.

Lesenswert sind:

• Per Martin-Löf: Intuitionistic Type Theory., Studies in Proof Theory Lecture Notes, Bibliopolis, Napoli 2002
• Robert L. Constable et. al.: Implementing Mathematics with the Nuprl proof development system. Prentice Hall, 1986
• Lawrence C. Paulson: Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, 1987
• Jean-Yves Girard, Yves Lafont, and Paul Taylor: Proofs and Types. Cambridge University Press, 1989
• Bengt Nordström , Kent Petersson, and Jan M. Smith: Programming in Martin-Löf's Type Theory. An introduction. Clarendon Press, Oxford, 1990

online bereitgestellt werden:

• Ein ausführliches Skript und die Folien der Vorlesung.
• das Nuprl Manual

Programme

• Nuprl kann via Remote-Zugriff auf einen unserer Server probiert werden. Hier eine Kurzanleitung.
  Die offizielle Nuprl Webseite ist www.nuprl.org. Hier findet man eine Version des Systems zur Selbstinstallation und viel Hintergrundmaterial.
• Das Isabelle System unterstützt eine klassische Typentheorie und sehr leistungsfähige Taktiken.
• Das MetaPRL System ist eine Neu-Implementierung von Nuprl, die auf verschiedenen Platformen arbeitet.
• Das Coq System unterstützt eine verwandte Typentheorie, den Calculus of Constructions,