Some Notes on Inductive and Co-Inductive Techniques in the Semantics of Functional Programs DRAFT VERSION

These notes were handed out at a course on Inductive and Co-Inductive Techniques in the Semantics of Functional Programs given by Andrew Pitts, The Computer Laboratory, Cambridge University, while visiting BRICS 21 November - 2 December 1994. The course material included these notes, the report Relational Properties of Domains and slides.

Course Description
The aim of the course is to describe recent advances in formal techniques for establishing observational equivalence of functional programs. It considers both operational and denotational methods and the relationship between them. One goal is to give an exposition of Howe's method for characterizing observational equivalence as a co-inductively defined ``applicative bisimulation''. Another goal is to describe Freyd's analysis of recursively defined domains in terms of a property of mixed initiality/finality. Applications of this are given to proving correspondence of operational and denotational semantics and to inductive and co-inductive reasoning about ``user-declared'' datatypes.

Abstract: