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 (leider nicht ganz aktuelle) 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,