[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs@csl.sri.com*From*: Prototype Verification System <pvs@turing.une.edu.au>*Date*: Tue, 1 May 2001 11:11:23 +1000*Sender*: pvs-owner@csl.sri.com

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

- Prev by Date:
**Re: More questions about predicate subtypes** - Next by Date:
**paperback announcement: Categorical Logic and Type Theory** - Prev by thread:
**No Subject** - Next by thread:
**No Subject** - Index(es):