An Indexed Model of Impredicative Polymorphism and Mutable References
Amal Ahmed, Andrew W. Appel, Roberto Virga · 2003
We present a semantic model of the polymorphic lambda calculus augmented with a higher-order store, allowing the storage of values of any type, including impredicative quantified types, mutable references, recursive types, and functions. Our model provides the first denotational semantics for a type system with updatable references to values of impredicative quantified types. The central idea behind our semantics is that instead of tracking the exact type of a mutable reference in a possible world our model keeps track of the approximate type. While high-level languages like ML and Java do not themselves support storage of impredicative existential packages in mutable cells, this feature is essential when representing ML function closures, that is, in a target language for typed closure conversion of ML programs.