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.