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...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Benjamin C. Pierce, Michael Greenberg, Stephanie Weirich
• Keywords: Latent Contracts, Manifest Calculus H, Manifest Contracts, POPL 2010, Programming Languages