equal
deleted
inserted
replaced
|
1 <HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY> |
|
2 |
|
3 <H2>CTT: Constructive Type Theory</H2> |
|
4 |
|
5 This directory contains the Standard ML sources of the Isabelle system for |
|
6 Constructive Type Theory (extensional equality, no universes). Important |
|
7 files include |
|
8 |
|
9 <DL> |
|
10 <DT>ROOT.ML |
|
11 <DD>loads all source files. Enter an ML image containing Pure |
|
12 Isabelle and type: use "ROOT.ML";<P> |
|
13 |
|
14 <DT>Makefile |
|
15 <DD>compiles the files under Poly/ML or SML of New Jersey<P> |
|
16 |
|
17 <DT>ex |
|
18 <DD>subdirectory containing examples. To execute them, enter an ML image |
|
19 containing CTT and type: use "ex/ROOT.ML";<P> |
|
20 </DL> |
|
21 |
|
22 Useful references on Constructive Type Theory: |
|
23 |
|
24 <UL> |
|
25 <LI> B. Nordström, K. Petersson and J. M. Smith,<BR> |
|
26 Programming in Martin-Löf's Type Theory<BR> |
|
27 (Oxford University Press, 1990) |
|
28 |
|
29 <LI> Simon Thompson,<BR> |
|
30 Type Theory and Functional Programming (Addison-Wesley, 1991) |
|
31 </UL> |
|
32 </BODY></HTML> |