Oxford University
4pm Thursday, 17th of March, 2009
Room 4.31/4.33, Informatics Forum
We present the first effectively presentable fully abstract model for Stark's Reduced ML, the paradigmatic higher-order programming language combining call-by-value evaluation and integer-valued references.
The model is constructed using techniques of nominal game semantics. Its distinctive feature is the presence of carefully restricted information about the store in plays, combined with conditions concerning the participants' ability to distinguish reference names. This leads to an explicit characterization of program equivalence.
This is joint work with Nikos Tzevelekos.