Typed Operational Reasoning (Abstract)
The aim of this chapter is to explain, by example, some methods for
reasoning about equivalence of programs based directly upon a type
system and an operational semantics for the programming language in
question. We will concentrate on methods for reasoning about
equivalence of representations of abstract data types. This provides
an excellent example: it is easy to appreciate why such methods are
useful and at the same time non-trivial problems have to be solved to
get a sound reasoning principle in the presence of non-termination and
recursion. Rather than just treat abstract data types, we will cover
full existential types, using a programming language combining a pure
fragment of ML (including records and recursive functions) with System
F. β
Last modified: Wed Aug 25 20:02:10 BST 2004