Full abstraction for Reduced ML

&
Annals of Pure and Applied Logic 164 (11):1118-1143 (2013)
  Copy   BIBTEX

Abstract

We present the first effectively presentable fully abstract model for Starkʼs Reduced ML, a call-by-value higher-order programming language featuring 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. We show how it leads to an explicit characterization of program equivalence

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2013.05.007

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 101,394

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A game semantics of names and pointers.J. Laird - 2008 - Annals of Pure and Applied Logic 151 (2-3):151-169.
Angelic semantics of fine-grained concurrency.Dan R. Ghica & Andrzej S. Murawski - 2008 - Annals of Pure and Applied Logic 151 (2-3):89-114.
An approach to deciding the observational equivalence of Algol-like languages.C. -H. L. Ong - 2004 - Annals of Pure and Applied Logic 130 (1-3):125-171.
Infinite trace equivalence.Paul Blain Levy - 2008 - Annals of Pure and Applied Logic 151 (2-3):170-198.
An infinite-game semantics for well-founded negation in logic programming.Chrysida Galanaki, Panos Rondogiannis & William W. Wadge - 2008 - Annals of Pure and Applied Logic 151 (2-3):70-88.
Second-order type isomorphisms through game semantics.Joachim de Lataillade - 2008 - Annals of Pure and Applied Logic 151 (2-3):115-150.
On the unity of duality.Noam Zeilberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):66-96.
Linear realizability and full completeness for typed lambda-calculi.Samson Abramsky & Marina Lenisa - 2005 - Annals of Pure and Applied Logic 134 (2-3):122-168.
An Axiomatic Account of a Fully Abstract Game Semantics for General References.Jim Laird & Guy McCusker - 2023 - In Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Verlag. pp. 251-292.
Deconstructing General References via Game Semantics.Andrzej S. Murawski & Nikos Tzevelekos - 2023 - In Alessandra Palmigiano & Mehrnoosh Sadrzadeh (eds.), Samson Abramsky on Logic and Structure in Computer Science and Beyond. Springer Verlag. pp. 293-325.

Analytics

Added to PP
2013-12-12

Downloads
40 (#562,114)

6 months
6 (#861,180)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Full abstraction for Reduced ML.Andrzej S. Murawski & Nikos Tzevelekos - 2013 - Annals of Pure and Applied Logic 164 (11):1118-1143.

Add more citations

References found in this work

Full abstraction for Reduced ML.Andrzej S. Murawski & Nikos Tzevelekos - 2013 - Annals of Pure and Applied Logic 164 (11):1118-1143.
A game semantics of names and pointers.J. Laird - 2008 - Annals of Pure and Applied Logic 151 (2-3):151-169.

Add more references