Higher-Order and Symbolic Computation, 16(3)161-202
Formal Foundations of Operational SemanticsJonathan Ford, School of Mathematics, Statistics, & Computing Science University of New England Armidale, NSW 2351 Australia
Ian A. Mason, School of Mathematics, Statistics, & Computing Science University of New England Armidale, NSW 2351 Australia
|
Abstract: In this paper we report on the results of a
sophisticated and substantial use of PVS to establish a recent result
in operational semantics. The result we establish is a context lemma
for operational equivalence for very wide class of programming
languages, known as the CIU theorem. The proof uses the annotated
holes technique to represent contexts and compute with them. Thus this
paper demonstrates that that it is possible to use PVS as a tool in
the development of modern operational techniques, and a productive
tool at that. The process of formalizing the CIU theorem revealed
several gaps in published proof. The proof of the CIU theorem in PVS
took approximately six months to develop. The actual machine checked
proof involves the proving of around one thousand facts, and takes PVS
slightly less than three hours of CPU time running on a Linux machine
configured with 2 GBytes of main memory and four 550 MHz Xeon PIII
processors.
Keywords: lambda-calculus, contexts, operational semantics, theorem proving, PVS |
This article can be downloaded [here].
![[picture of journal cover]](../LISP.JPG)