Operational semantics and program equivalence

Abstract. This tutorial paper discusses a particular style of operational semantics that enables one to give a ‘syntax-directed ’ inductive definition of termination which is very useful for reasoning about operational equivalence of programs. We restrict attention to contextual equivalence of expressions in the ML family of programming languages, concentrating on functions involving local state. A brief tour of structural operational machine using ‘frame stacks’. Applications of this to reasoning about contextual equivalence are given