equal
deleted
inserted
replaced
|
1 Cube: Barendregt's Lambda-Cube |
|
2 |
|
3 This directory contains the Standard ML sources of the Isabelle system for |
|
4 the Lambda-Cube. Important files include |
|
5 |
|
6 ROOT.ML -- loads all source files. Enter an ML image containing Pure |
|
7 Isabelle and type: use "ROOT.ML"; |
|
8 |
|
9 Makefile -- compiles the files under Poly/ML or SML of New Jersey |
|
10 |
|
11 ex.ML -- examples file. To execute them, enter an ML image |
|
12 containing Cube and type: use "ex.ML"; |
|
13 |
|
14 NB: the formalization is not completely sound! It does not enforce |
|
15 distinctness of variable names in contexts! |
|
16 |
|
17 For more information about the Lambda-Cube, see |
|
18 H. Barendregt |
|
19 Introduction to Generalised Type Systems |
|
20 J. Functional Programming |
|
21 |