Sciweavers

Share
TLDI
2009
ACM

Relational parametricity for references and recursive types

11 years 10 months ago
Relational parametricity for references and recursive types
We present a possible world semantics for a call-by-value higherorder programming language with impredicative polymorphism, general references, and recursive types. The model is one of the first relationally parametric models of a programming language with all these features. To model impredicative polymorphism we define the semantics of types via parameterized (world-indexed) logical relations over a universal domain. It is well-known that it is non-trivial to show the existence of logical relations in the presence of recursive types. Here the problems are exacerbated because of general references. We explain what the problems are and present our solution, which makes use of a novel approach to modeling references. We prove that the resulting semantics is adequate with respect to a standard operational semantics and include simple examples of reasoning about contextual equivalence via parametricity. Categories and Subject Descriptors F.3.2 [Logics and Meanings of Programs]: Semanti...
Lars Birkedal, Kristian Støvring, Jacob Tha
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2009
Where TLDI
Authors Lars Birkedal, Kristian Støvring, Jacob Thamsborg
Comments (0)
books