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