Mechanized operational semantics via (Co)induction

Abstract

We give a fully automated description of a small 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 of this paper is a fully automated proof that PL bisimulation coincides with PL contextual equivalence.