A BRICS Mini-Course
June 10 and 11, 2004
Lectures by
Patricia Johann, pjohann@crab.rutgers.edu
Department of Computer Science, Rutgers University
Free theorems are often used to justify applications of program transformations based on rank-2 polymorphic combinators in languages derived from the Girard-Reynolds polymorphic lambda calculus. Examples of such transformations are the foldr/build and destroy/unfoldr rules for eliminating intermediate data structures from compositions involving polymorphic functions. While free theorems can indeed be used to prove correctness and related properties of such transformations, several subtle-but-critical issues associated with doing so are routinely left unaddressed. This results in justifications for applications of free theorems-based transformations which hold only if some highly non-trivial assumptions are made.
In this mini-course, I will make explicit these (usually implicit) assumptions, and highlight their importance for formalizing correctness proofs for program transformations based on free theorems. I will also argue that most invocations of free theorems to justify applications of program transformations do not properly address the issues which make these assumptions necessary. Finally, I will describe in detail an operational semantics-based approach to deriving free theorems which does properly address these issues, and thus makes possible formal correctness proofs for transformations based on free theorems in those settings in which it is available.