Full abstraction for nominal general references

DOI10.2168/LMCS-5(3:8)2009MaRDI QIDQ3401132zbMATH OpenOpenAlexFDO

Authors Nikos Tzevelekos

Publication date 28 January 2010

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0907.4477

zbMATH Keywords

\(\nu\)-calculuscomonadsdenotational semanticsgame semanticsMLmonads

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Abstract: Game semantics has been used with considerable success in formulating fully abstract semantics for languages with higher-order procedures and a wide range of computational effects. Recently, nominal games have been proposed for modelling functional languages with names. These are ordinary, stateful games cast in the theory of nominal sets developed by Pitts and Gabbay. Here we take nominal games one step further, by developing a fully abstract semantics for a language with nominal general references.

Recommendations

• Game semantics for nominal exceptions
• Denotational semantics with nominal Scott domains
• Towards nominal Abramsky
• Operational nominal game semantics
• A game semantics of names and pointers

Cited in

(23)

• Algorithmic games for full ground references
• A game semantics of names and pointers
• Game semantics for access control
• Definability and full abstraction
• Full abstraction for nominal Scott domains
• Operational nominal game semantics
• Block structure vs scope extrusion: between innocence and omniscience
• Game semantics in the nominal model
• Full abstraction for Reduced ML
• Program equivalence in a simple language with state
• Deconstructing general references via game semantics
• Towards nominal Abramsky
• Combining and relating control effects and their semantics
• Polynomial-time equivalence testing for deterministic fresh-register automata
• Foundations of Software Science and Computation Structures
• Game semantics for nominal exceptions
• Global state considered helpful
• A Fully Abstract Trace Semantics for General References
• Denotational semantics with nominal Scott domains
• Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
• An axiomatic account of a fully abstract game semantics for general references
• Towards univalent reference types: the impact of univalence on denotational semantics
• Fully abstract normal form bisimulation for call-by-value PCF

This page was built for publication: Full abstraction for nominal general references

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3401132)