## 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)