Full Abstraction for Reduced ML

traction for Reduced ML Andrzej S. Murawski and Nikos Tzevelekos Oxford University Computing Laboratory Wolfson Building, Parks Road, Oxford OX1 3QD, UK 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.

• Type: Conference
• Year: 2009
• Where: FOSSACS
• Authors: Andrzej S. Murawski, Nikos Tzevelekos
• Keywords: Applied Computing, FOSSACS 2009, Language Combining Call-by-value, Oxford University Computing Laboratory, Stark’s Reduced ML