NameDateSize

..25-Jul-20199

chap11_1Script.smlH A D25-Jul-201921.7 KiB

chap2Script.smlH A D25-Jul-201922.1 KiB

chap3Script.smlH A D25-Jul-201955.1 KiB

finite_developmentsScript.smlH A D25-Jul-2019172.4 KiB

head_reductionScript.smlH A D25-Jul-201912.4 KiB

HolmakefileH A D25-Jul-201949

labelledTermsScript.smlH A D25-Jul-201918.8 KiB

normal_orderScript.smlH A D25-Jul-201938.7 KiB

READMEH A D25-Jul-20191.5 KiB

reductionEval.sigH A D25-Jul-2019389

reductionEval.smlH A D25-Jul-201912.1 KiB

standardisationScript.smlH A D25-Jul-201999.3 KiB

takahashiScript.smlH A D25-Jul-20194.1 KiB

term_posnsScript.smlH A D25-Jul-201922.7 KiB

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