Contracts made manifest

Michael Greenberg, Benjamin C. Pierce, Stephanie Weirich

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

37 Scopus citations

Abstract

Since Findler and Felleisen 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, 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 dependent contracts , whose predicates can mention free variables. This extension is both pragmatically crucial, supporting a much more interesting range of contracts, and theoretically challenging. We define dependent versions of λH and two dialects ("lax" and "picky") of λC, establish type soundness - a substantial result in itself, for λH - and extend φ and ψ accordingly. Surprisingly, the intuition that the latent and manifest systems are equivalent now breaks down: the extended translations preserve behavior in one direction but, in the other, sometimes yield terms that blame more.

Original languageEnglish
Title of host publicationPOPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages353-364
Number of pages12
DOIs
StatePublished - 2010
Event37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10 - Madrid, Spain
Duration: 17 Jan 201023 Jan 2010

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Conference

Conference37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10
Country/TerritorySpain
CityMadrid
Period17/01/1023/01/10

Keywords

  • Blame
  • Contract
  • Dynamic checking
  • Postcondition
  • Precondition
  • Refinement type
  • Translation

Fingerprint

Dive into the research topics of 'Contracts made manifest'. Together they form a unique fingerprint.

Cite this