Operational Semantics and Program Equivalence

13 years 8 months ago
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
Andrew M. Pitts
Added 01 Aug 2010
Updated 01 Aug 2010
Type Conference
Year 2000
Where AC
Authors Andrew M. Pitts
Comments (0)