Mechanical Verification of a Context Lemma


We are very pleased to announce the completion of a mechanically
verified proof of recent result in operational semantics, using SRI's
PVS system.  The result is a context lemma for a general class of
programming languages, and goes by the name of the "CIU lemma".  The
proof uses the "annotated holes" technique developed in [1] to prove
the original version of the CIU lemma. The actual version of the lemma
we prove is much more general than [1], and follows the development of
[2]. An paper describing the result, and the proof development, can be
found at [3], and the actual machine proof at [4], in the form of a
PVS dump file. The development of the proof uncovered several small
gaps in the presentation given in [2].

The actual proof of CIU in PVS involves the proving over one thousand
distinct facts.  It takes PVS 9248 seconds (154 minutes) of
CPU time running on a Linux machine configured with 2GBytes of main
memory and 4 550 MHz Xeon PIII processors.  The dump file containing
all the PVS definitions, facts, and proofs is 17 MBytes and is
available from [4]

[1] Mason, I. A. and Talcott, C. L.,
Equivalence in Functional Languages with Effects,
Journal of Functional Programming, Vol 1, pp 287-327, 1991.
Available as postscript from 

[2] Talcott, C.,
Reasoning about Functions with Effects,
in "Higher Order Operational Techniques in Semantics",
Gordon, A. D. and Pitts, A. M. (Editors),
Cambridge University Press, 1996.

[3] Ford , J. and Mason, I. A.,
Establishing a  General Context Lemma in PVS,
Proceedings of the 2nd Australasian Workshop on Computational Logic, AWCL'01,
Available as postscript from 

[4] http://mcs.une.edu.au/~pvs/

Jonathan Ford & Ian A. Mason
University of New England

------- End of forwarded message -------