BRICS · Contents · Programme · References

Proving Correctness of Program Transformations Based on Free Theorems

A BRICS Mini-Course
June 10 and 11, 2004

Lectures by
Patricia Johann, pjohann@crab.rutgers.edu
Department of Computer Science, Rutgers University


Course Contents

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.

Programme

Thursday June 10, 2004, 10:15-11:00 in Turing 016

Friday June 11, 2004, 10:15-12:00 in Turing 016

References

  1. Patricia Johann: Short Cut Fusion is Correct
  2. Andy Pitts: Parametric Polymorphism and Operational Equivalence