author | wenzelm |
Sat, 02 Apr 2016 23:29:05 +0200 | |
changeset 62826 | eb94e570c1a4 |
parent 58974 | cbc2ac19d783 |
child 63505 | 42e1dece537a |
permissions | -rw-r--r-- |
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
1 |
chapter CTT |
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
2 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset
|
3 |
session CTT = Pure + |
48475 | 4 |
description {* |
5 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
6 |
Copyright 1991 University of Cambridge |
|
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
7 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
8 |
This is a version of Constructive Type Theory (extensional equality, |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
9 |
no universes). |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
10 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
11 |
Useful references on Constructive Type Theory: |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
12 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
13 |
B. Nordström, K. Petersson and J. M. Smith, Programming in Martin-Löf's |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
14 |
Type Theory (Oxford University Press, 1990) |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
15 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
16 |
Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
17 |
1991) |
48475 | 18 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
19 |
options [document = false] |
58974 | 20 |
theories |
21 |
Main |
|
48475 | 22 |
|
58974 | 23 |
(* Examples for Constructive Type Theory *) |
24 |
"ex/Typechecking" |
|
25 |
"ex/Elimination" |
|
26 |
"ex/Equality" |
|
27 |
"ex/Synthesis" |