README
1dBScript.sml
2 develops a theory of (untyped) "locally nameless" de Bruijn terms.
3
4ncScript.sml
5 builds a theory of name-carrying terms, where terms are identified
6 up to alpha-conversion. This development underlies the paper
7
8 "5 Axioms of Alpha Conversion",
9 Andy Gordon and Tom Melham,
10 Proceedings of TPHOLs'96, Springer LNCS 1125.
11
12 Proves a recursion combinator for these terms as per the paper
13
14 "Recursive Function Definition for Types with Binders"
15 Michael Norrish
16 Proceedings of TPHOLs'2004, Springer LNCS 3223
17
18gmtermScript.sml
19 develops a theory of "traditional" lambda-calculus terms by
20 creating a type like that in ncScript, but without the CON
21 constructor.
22
23 ------------------------------
24
25diagsScript.sml
26 a type of rewriting style diagrams and how rewriting relations do
27 or do not satisfy them. Also a proof that "diagram-satisfaction"
28 is preserved and reflected by strong onto homomorphisms. (This is
29 discussed in the NICTA/JAIST technical report "Structural
30 preservation and reflection of diagrams", and is joint work with
31 Ren�� Vestergaard.)
32
33raw_syntaxScript.sml
34 proof that a raw syntax of lambda terms (not identified up to alpha
35 equivalence) with its own notions of substitution, alpha
36 equivalence and beta reduction can indeed be collapsed into the
37 type of terms from termTheory. Use diagrams to show confluence for
38 beta-alpha reduction at this raw level by appeal to result in
39 barendregt/chap3Theory.
40
41 ------------------------------
42
43string_numScript.sml
44 a proof by construction that strings and numbers are in bijection
45
46pure_dBScript.sml
47 mechanisation of the type of "pure" de Bruijn terms, following
48 Tobias Nipkow's paper "More Church-Rosser Proofs". (They are
49 "pure" in contrast with Andy Gordon's de Bruijn terms, which have
50 indices for bound variables and strings for free variables.)
51
52 Demonstration that this type and its notions of beta- and
53 eta-reduction are isomorphic to the quotiented type in termTheory.
54 This work is described in
55
56 "Proof Pearl: de~Bruijn Terms Really Do Work"
57 Michael Norrish and Ren�� Vestergaard
58 Proceedings of TPHOLs'2007, Springer LNCS 4732
59
60 ------------------------------
61
62MPlambdaScript.sml
63 Mechanisation of the McKinna-Pollack two-sorted lambda-calculus.
64
65 ------------------------------
66
67lnamelessScript.sml
68 Mechanisation of the approach from the POPL paper "Engineering
69 Formal Metatheory" by Brian Aydemir, Arthur Chargu��raud, Benjamin
70 Pierce, Randy Pollack and Stephanie Weirich. That paper is more
71 concerned with typing the simple lambda calculus than
72 beta-reduction, so that's what's covered here too. (Further, these
73 locally nameless terms are basically the same as Andy Gordon's dB
74 terms.)
75
76