Implementing Mathematics Using NuPrl
Full online text of the book. Includes tutorial on Martin-Löf's type theory, motivating remarks on intuitionism, as well as sample formalisations of constructive mathematics in the NuPrl theorem prover.