Preuves, Programmes et Systèmes

Nikos Tzevelekos (Department of Computer Science, University of Oxford)

Game semantics for good general references

Jeudi 29 septembre 2011, 11h salle 1D23

Abstract: We introduce a new fully abstract and effectively presentable denotational model for RefML, a paradigmatic higher-order programming language combining call-by-value evaluation and general references in the style of ML. Our model is built using game semantics. In contrast to the previous effectively presentable model by Abramsky, Honda and McCusker [AHM98], it provides a faithful account of reference types, and the full abstraction result does not rely on the availability of spurious constructs of reference type (bad variables). This is the first denotational model of this kind, preceded only by the trace model recently proposed by Laird [Lai07].

The talk presents our paper of the same title which appeared in LICS earlier this year.