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 -
![[TXT]](/icons/text.gif)
rew.ML.html 09-Aug-2008 06:09 0k
![[DIR]](/icons/folder.gif)
ex/ 09-Aug-2008 06:09 -
Main.thy.html 09-Aug-2008 06:09 0k
IsaMakefile.html 09-Aug-2008 06:09 2k
Bool.thy.html 09-Aug-2008 06:09 0k
Arith.thy.html 09-Aug-2008 06:09 0k
ROOT.ML.html 09-Aug-2008 06:09 0k
CTT.thy.html 09-Aug-2008 06:09 0k
CTT.ML.html 09-Aug-2008 06:09 0k
Bool.ML.html 09-Aug-2008 06:09 0k
Arith.ML.html 09-Aug-2008 06:09 0k
![[ ]](/icons/unknown.gif)
rew.ML 19-Sep-2005 23:22 1k
CTT.ML 19-Sep-2005 23:22 6k
ROOT.ML 16-Sep-2005 14:01 1k
Main.thy 16-Sep-2005 14:01 1k
CTT.thy 16-Sep-2005 14:01 8k
Bool.thy 16-Sep-2005 14:01 1k
Bool.ML 16-Sep-2005 14:01 1k
Arith.thy 16-Sep-2005 14:01 1k
Arith.ML 16-Sep-2005 14:01 12k
IsaMakefile 14-Nov-2000 04:26 1k
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)