Contracts Made Manifest

10 years 11 months ago
Contracts Made Manifest
Since Findler and Felleisen [2002] introduced higher-order contracts, many variants have been proposed. Broadly, these fall into two groups: some follow Findler and Felleisen in using latent contracts, purely dynamic checks that are transparent to the type system; others use manifest contracts, where refinement types record the most recent check that has been applied to each value. These two approaches are commonly assumed to be equivalent--different ways of implementing the same idea, one retaining a simple type system, and the other providing more static information. Our goal is to formalize and clarify this folklore understanding. Our work extends that of Gronski and Flanagan [2007], who defined a latent calculus C and a manifest calculus H, gave a translation from C to H, and proved that, if a C term reduces to a constant, then so does its -image. We enrich their account with a translation from H to C and prove an analogous theorem. We then generalize the whole framework to depe...
Benjamin C. Pierce, Michael Greenberg, Stephanie W
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Benjamin C. Pierce, Michael Greenberg, Stephanie Weirich
Comments (0)