Polymorphic manifest contracts, revised and resolved

Taro Sekiyama, Atsushi Igarashi, Michael Greenberg

Research output: Contribution to journalArticlepeer-review

9 Scopus citations

Abstract

Manifest contracts track precise program properties by refining types with predicates-for example, {x:Int | x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give strong contracts to abstract types, precisely stating pre- and post conditions while hiding implementation details-for instance, an abstract type of stacks might specify that the pop operation has input type {x:αStack | not (empty x)}. This article studies a polymorphic calculus with manifest contracts and establishes fundamental properties including type soundness and relational parametricity. Indeed, this is not the first work on polymorphic manifest contracts, but existing calculi are not very satisfactory. Gronski et al. developed the SAGE language, which introduces polymorphism through the Type:Type discipline, but they do not study parametricity. Some authors of this article have produced two separate works: Belo et al. [2011] and Greenberg [2013] studied polymorphic manifest contracts and parametricity, but their calculi have metatheoretical problems in the type conversion relations. Indeed, they depend on a few conjectures, which turn out to be false. Our calculus is the first polymorphic manifest calculus with parametricity, depending on no conjectures-it resolves the issues in prior calculi with delayed substitution on casts.

Original languageEnglish
Article number3
JournalACM Transactions on Programming Languages and Systems
Volume39
Issue number1
DOIs
StatePublished - Feb 2017

Keywords

  • Abstract datatypes
  • Contracts
  • Corrections
  • Dynamic checking
  • Logical relations
  • Parametric polymorphism
  • Postconditions
  • Preconditions
  • Refinement types
  • Runtime verification
  • Syntactic proof

Fingerprint

Dive into the research topics of 'Polymorphic manifest contracts, revised and resolved'. Together they form a unique fingerprint.

Cite this