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