|
|
Named variable proof of Church-Rosser for the call-by-value lambda calculus
[2.4Meg cr.dmp]
[174k cr.dmp.Z]
Operational Techniques in PVS - A Preliminary Evaluation.
Jonathan Ford and Ian A. Mason.
Proceedings of Computing: the Australian Theory Symposium.
(CATS 2001)
[ps]
[dvi]
[pdf]
[bibtex cite]
Proof of the (generalized) CIU Theorem (with corrected trichotomy axiom).
[17 Meg Ciu.dmp]
[0.8 Meg Ciu.dmp.Z]
Establishing a General Context Lemma in PVS.
Jonathan Ford and Ian A. Mason.
Proceedings of the 2nd Australasian Workshop on Computational Logic, (AWCL'01)
[ps]
[dvi]
[pdf]
[bibtex cite]
Formal Verification and Operational Semantics.
Jonathan Ford.
Jonathan Ford's 4th year Honours Thesis.
[ps]
[dvi]
[pdf]
