[Prev][Next][Index][Thread]
Mechanical Verification of a Context Lemma
People,
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
http://mcs.une.edu.au/~iam/Data/Papers/91fp.ps
[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.
http://steam.stanford.edu/MT/96hoots.ps.Z
[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
http://mcs.une.edu.au/~iam/Data/Papers/01awcl.ps
[4] http://mcs.une.edu.au/~pvs/
Jonathan Ford & Ian A. Mason
University of New England
Armidale
Australia
------- End of forwarded message -------