equal
deleted
inserted
replaced
1 CTT: Constructive Type Theory |
|
2 |
|
3 This directory contains the Standard ML sources of the Isabelle system for |
|
4 Constructive Type Theory (extensional equality, no universes). Important |
|
5 files include |
|
6 |
|
7 ROOT.ML -- loads all source files. Enter an ML image containing Pure |
|
8 Isabelle and type: use "ROOT.ML"; |
|
9 |
|
10 Makefile -- compiles the files under Poly/ML or SML of New Jersey |
|
11 |
|
12 ex -- subdirectory containing examples. To execute them, enter an ML image |
|
13 containing CTT and type: use "ex/ROOT.ML"; |
|
14 |
|
15 Useful references on Constructive Type Theory: |
|
16 |
|
17 B. Nordstr\"om, K. Petersson and J. M. Smith, |
|
18 Programming in Martin-L\"of's Type Theory |
|
19 (Oxford University Press, 1990) |
|
20 |
|
21 Simon Thompson, |
|
22 Type Theory and Functional Programming (Addison-Wesley, 1991) |
|
23 |
|