Operational Semantics and Program Equivalence

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 semantics culminates in a structural definition of termination via an abstract machine using ‘frame stacks’. Applications of this to reasoning about contextual equivalence are given. Table of Contents

• Type: Conference
• Year: 2000
• Where: AC
• Authors: Andrew M. Pitts
• Keywords: AC 2000, Contextual Equivalence, Operational Equivalence, Operational Semantics, Software Engineering