Index of /ports/math/isabelle/work/Isabelle/src/CTT
Name Last modified Size Description
![[DIR]](/icons/back.gif)
Parent Directory 09-Aug-2008 06:09 -
![[ ]](/icons/unknown.gif)
Arith.ML 16-Sep-2005 14:01 12k
![[TXT]](/icons/text.gif)
Arith.ML.html 09-Aug-2008 06:09 0k
Arith.thy 16-Sep-2005 14:01 1k
Arith.thy.html 09-Aug-2008 06:09 0k
Bool.ML 16-Sep-2005 14:01 1k
Bool.ML.html 09-Aug-2008 06:09 0k
Bool.thy 16-Sep-2005 14:01 1k
Bool.thy.html 09-Aug-2008 06:09 0k
CTT.ML 19-Sep-2005 23:22 6k
CTT.ML.html 09-Aug-2008 06:09 0k
CTT.thy 16-Sep-2005 14:01 8k
CTT.thy.html 09-Aug-2008 06:09 0k
IsaMakefile 14-Nov-2000 04:26 1k
IsaMakefile.html 09-Aug-2008 06:09 2k
Main.thy 16-Sep-2005 14:01 1k
Main.thy.html 09-Aug-2008 06:09 0k
ROOT.ML 16-Sep-2005 14:01 1k
ROOT.ML.html 09-Aug-2008 06:09 0k
![[DIR]](/icons/folder.gif)
ex/ 09-Aug-2008 06:09 -
rew.ML 19-Sep-2005 23:22 1k
rew.ML.html 09-Aug-2008 06:09 0k
CTT/README
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)