A BRICS Mini-Course
November 22, 24 and 29, December 1, 1994
Lectures by
Andrew Pitts
The Computer Laboratory, Cambridge University
The aim of the course will be to describe recent advances in formal techniques for establishing observational equivalence of functional programs. We will consider both operational and denotational methods and the relationship between them. One goal will be to give an exposition of Howe's method for characterizing observational equivalence as a co-inductively defined ``applicative bisimulation''. Another goal will be to describe Freyd's analysis of recursively defined domains in terms of a property of mixed initiality/finality. We will give applications of this to proving correspondence of operational and denotational semantics and to inductive and co-inductive reasoning about ``user-declared'' datatypes.
In addition, Andrew Pitts will give a more generally accessible lecture, on the topic of the course, in the DAIMI lecture series Wednesday 30 November, 15.15-16.00.
The course should be of interest to students and researchers interested in the semantics and logics of programs. The course has as prerequisites some knowledge of domain theory and introductory category theory, though the early lectures could be more broadly understandable.