README
1sttScript.sml
2 * define a notion of simple type ("stype"), with --> a binary
3 constructor and one base type (called "base").
4 * define a typing "context", a list of string#stype pairs, the
5 notion of permutation over contexts, and thus their support
6 (ctxtFV).
7 * define the standard simple typing relation for ��-calculus terms.
8 * prove
9 - typing contexts can be enlarged ("weakening")
10 - typing contexts can be permuted
11 - typing contexts can drop all mappings except for the variables
12 in the term being typed
13 - typing is preserved by ��-reduction (from
14 barendregt/chap3Theory)
15 - and a bunch of other supporting lemmas
16
17sttVariants.sml
18 Suggested by Randy Pollack:
19 * A proof that the original typing relation from sttTheory is
20 equivalent to another relation which has an infinitary
21 (universally quantified) hypothesis in the rule for the
22 abstraction case, and where the body under the universal involves
23 a substitution.
24 * Also, derive a similar induction principle directly for the
25 original typing relation (this one in the style of "engineering
26 meta-theory" paper from POPL 2008).
27
28type_schemasScript.sml
29 Demonstration of how to construct a type where a binder takes a set
30 of names as an argument. This is done in type schemas in the
31 Hindley-Milner typing system, where the universal quantifiers bind
32 over sets of type variables.
33