By João Filipe Belo and Michael Greenberg and Atsushi Igarashi and Benjamin C. Pierce. In Proceedings of European Symposium on Programming (ESOP2011), volume 6602 of Springer LNCS, pages 18-37, Saarbrücken, Germany, March, 2011.
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 in- put type {x : α Stack | not (empty x )}. We formalize this combination by defining FH , a polymorphic calculus with manifest contracts, and estab- lishing fundamental properties including type soundness and relational parametricity. Our development relies on a significant technical improve- ment 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.
$Date: $