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öm, K. Petersson and J. M. Smith,
Programming in Martin-Löf's Type Theory
(Oxford University Press, 1990)
- Simon Thompson,
Type Theory and Functional Programming (Addison-Wesley, 1991)