CTT: Constructive Type Theory
This directory contains the Standard ML sources of the Isabelle system for
Constructive Type Theory (extensional equality, no universes). Important
files include
ROOT.ML -- loads all source files. Enter an ML image containing Pure
Isabelle and type: use "ROOT.ML";
Makefile -- compiles the files under Poly/ML or SML of New Jersey
ex -- subdirectory containing examples. To execute them, enter an ML image
containing CTT and type: use "ex/ROOT.ML";
Useful references on Constructive Type Theory:
B. Nordstr\"om, K. Petersson and J. M. Smith,
Programming in Martin-L\"of's Type Theory
(Oxford University Press, 1990)
Simon Thompson,
Type Theory and Functional Programming (Addison-Wesley, 1991)