@inproceedings{a89ac5e2cdea4b4f8e84fc721bafc387,
title = "Polymorphic contracts",
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.",
keywords = "abstract datatypes, contracts, dynamic checking, logical relations, parametric polymorphism, postconditions, preconditions, refinement types, subtyping, syntactic proof",
author = "Belo, \{Jo{\~a}o Filipe\} and Michael Greenberg and Atsushi Igarashi and Pierce, \{Benjamin C.\}",
year = "2011",
doi = "10.1007/978-3-642-19718-5\_2",
language = "English",
isbn = "9783642197178",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "18--37",
booktitle = "Programming 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",
note = "20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 ; Conference date: 26-03-2011 Through 03-04-2011",
}