NameDateSize

..25-Jul-20199

dBScript.smlH A D25-Jul-201922.7 KiB

diagsScript.smlH A D25-Jul-201914.4 KiB

gmtermScript.smlH A D25-Jul-201923.1 KiB

hoasScript.smlH A D25-Jul-20194.1 KiB

HolmakefileH A D25-Jul-201961

lnamelessScript.smlH A D25-Jul-201916.2 KiB

MPlambdaScript.smlH A D25-Jul-201933.4 KiB

ncScript.smlH A D25-Jul-201943.1 KiB

pure_dBScript.smlH A D25-Jul-201942.7 KiB

raw_syntaxScript.smlH A D25-Jul-201925.5 KiB

READMEH A D25-Jul-20192.9 KiB

swapScript.smlH A D25-Jul-201925.9 KiB

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