src/CTT/README.html
author nipkow
Thu, 11 Jul 2002 10:48:30 +0200
changeset 13347 867f876589e7
parent 3279 815ef5848324
child 15283 f21466450330
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     1
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     2
<HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     3
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     4
<H2>CTT: Constructive Type Theory</H2>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     5
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     6
This directory contains the ML sources of the Isabelle system for
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     7
Constructive Type Theory (extensional equality, no universes).<p>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     8
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
     9
The <tt>ex</tt> subdirectory contains some examples.<p>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    10
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    11
Useful references on Constructive Type Theory:
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    12
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    13
<UL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    14
<LI>	B. Nordström, K. Petersson and J. M. Smith,<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    15
	Programming in Martin-Löf's Type Theory<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    16
	(Oxford University Press, 1990)
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    17
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    18
<LI>	Simon Thompson,<BR>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    19
	Type Theory and Functional Programming (Addison-Wesley, 1991)
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    20
</UL>
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    21
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    22
</BODY>
815ef5848324 tuned all READMEs;
wenzelm
parents: 1341
diff changeset
    23
</HTML>