README
1chap2Script.sml :
2 mechanisation of chapter 2 of Hankin's "Lambda calculi:
3 a guide for computer scientists"
4
5chap3Script.sml :
6 mechanisation of much of chapter 3 of Hankin with bits
7 of Barendregt's chapter 3 thrown in too
8
9chap11_1Script.sml :
10 mechanisation of section 11.1 from Barendregt's "The
11 lambda calculus: its syntax and semantics"
12
13term_posnsScript.sml :
14 establishes a type for labelling reductions, and
15 positions within terms more generally
16
17finite_developmentsScript.sml :
18 Barendregt's proof of the finite-ness of developments
19 (section 11.2), mechanising this notion as well as that
20 of residuals.
21
22standardisationScript.sml :
23 Barendregt's proof of the standardisation theorem, from
24 section 11.4.
25
26preltermScript.sml ltermScript.sml :
27 script files that establish the type of lambda calculus
28 terms with labelled redexes. Called $\Lambda'$ in
29 Barendregt.
30
31 ------------------------------
32
33These files are behind the papers:
34
35 "Mechanising Hankin and Barendregt using the Gordon-Melham axioms"
36 Michael Norrish
37 Proceedings of the Merlin 2003 Workshop
38
39and
40
41 "Mechanising \lambda-calculus using a classical first order theory
42 of terms with permutations"
43 Michael Norrish
44 In "Higher Order and Symbolic Computation", 19:169-195, 2006.
45