Hostname: page-component-7c8c6479df-995ml Total loading time: 0 Render date: 2024-03-28T11:53:21.478Z Has data issue: false hasContentIssue false

On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi

Published online by Cambridge University Press:  14 March 2005

PATRICIA JOHANN
Affiliation:
Department of Computer Science, Rutgers University, Camden, NJ 08102 USA Email: pjohann@crab.rutgers.edu

Abstract

A number of program transformations currently of interest can be derived from Wadler's ‘free theorems’ for calculi approximating modern functional languages. Although delicate but fundamental issues arise in proving the correctness of free theorems-based program transformations, these issues have usually been left unaddressed in the correctness proofs appearing in the literature. As a result, most such proofs are incomplete, and most free theorems-based transformations are applied to programs in calculi for which they are not actually known to be correct.

The purpose of this paper is three-fold. First, we raise and clarify some of the issues that must be addressed when constructing correctness proofs for free theorems-based program transformations. Second, we offer a principled approach to developing such proofs. Third, we use Pitts' recent work on parametricity and observational equivalence to show how our approach can be used to give the first proof that transformations based on the Acid Rain theorems preserve observational equivalence of programs in a polymorphic lambda calculus supporting FPC-style fixpoints and algebraic data types. Correctness of the foldr-build rule, the destroy-unfoldr rule, and the hylofusion program transformation for this calculus follows immediately. The same approach is expected to yield complete correctness proofs for free theorems-based transformations in calculi that even more closely resemble languages with which programmers are concerned in practice.

Type
Paper
Copyright
2005 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)