## CTT: Constructive Type Theory

This directory contains the ML sources of the Isabelle system for
Constructive Type Theory (extensional equality, no universes).
The `ex` subdirectory contains some examples.

Useful references on Constructive Type Theory:

- B. Nordstrm, K. Petersson and J. M. Smith,

Programming in Martin-Lf's Type Theory

(Oxford University Press, 1990)
- Simon Thompson,

Type Theory and Functional Programming (Addison-Wesley, 1991)