A MECHANIZED ACCOUNT OF PROGRAM EQUIVALENCE
Dr Simon Ambler, Department of Mathematics and Computer Science, University of Leicester

Abstract: This talk will describe some of the work I have been doing jointly with Roy Crole on mechanized operational semantics. We give a fully automated description of a small (functional) programming language PL in the theorem prover Isabelle98. The language syntax and semantics are encoded, and we formally verify a range of semantic properties. This is achieved via uniform (co)inductive methods. We encode notions of bisimulation and contextual equivalence. The main original contribution is to give a fully automated proof that PL bisimulation coincides with PL contextual equivalence.

This seminar was held at the Department of Computer Science, Royal Holloway, University of London on 22nd November, 1999.

back