Polymorphic contracts

João Filipe Belo, Michael Greenberg, Atsushi Igarashi, Benjamin C. Pierce

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

17 Scopus citations

Abstract

Manifest contracts track precise properties by refining types with predicates-e.g., {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 example, an abstract type of stacks might specify that the pop operation has input type {x :α Stack |not ( empty x )} . We formalize this combination by defining FH, a polymorphic calculus with manifest contracts, and establishing fundamental properties including type soundness and relational parametricity. Our development relies on a significant technical improvement over earlier presentations of contracts: instead of introducing a denotational model to break a problematic circularity between typing, subtyping, and evaluation, we develop the metatheory of contracts in a completely syntactic fashion, omitting subtyping from the core system and recovering it post facto as a derived property.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Proceedings
Pages18-37
Number of pages20
DOIs
StatePublished - 2011
Event20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 - Saarbrucken, Germany
Duration: 26 Mar 20113 Apr 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6602 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011
Country/TerritoryGermany
CitySaarbrucken
Period26/03/113/04/11

Keywords

  • abstract datatypes
  • contracts
  • dynamic checking
  • logical relations
  • parametric polymorphism
  • postconditions
  • preconditions
  • refinement types
  • subtyping
  • syntactic proof

Fingerprint

Dive into the research topics of 'Polymorphic contracts'. Together they form a unique fingerprint.

Cite this