Complete trace models of state and control
From MaRDI portal
Publication:2233464
DOI10.1007/978-3-030-72019-3_13zbMATH Open1473.68037arXiv2101.08491OpenAlexW3122294232MaRDI QIDQ2233464FDOQ2233464
Authors: Guilhem Jaber, Andrzej S. Murawski 
Publication date: 18 October 2021
Abstract: We consider a hierarchy of four typed call-by-value languages with either higher-order or ground-type references and with either callcc or no control operator.Our first result is a fully abstract trace model for the most expressive setting, featuring both higher-order references and callcc, constructed in the spirit of operational game semantics. Next we examine the impact of suppressing higher-order references and callcc in contexts and provide an operational explanation for the game-semantic conditions known as visibility and bracketing respectively.This allows us to refine the original model to provide fully abstract trace models of interaction with contexts that need not use higher-order references or callcc. Along the way, we discuss the relationship between error- and termination-based contextual testing in each case, and relate the two to trace and complete trace equivalence respectively.Overall, the paper provides a systematic development of operational game semantics for all four cases, which represent the state-based face of the so-called semantic cube.
Full work available at URL: https://arxiv.org/abs/2101.08491
Recommendations
- Trace semantics for polymorphic references
- Operational nominal game semantics
- A Fully Abstract Trace Semantics for General References
- Combining control effects and their models: game semantics for a hierarchy of static, dynamic and delimited control effects
- Game semantics for call-by-value polymorphism
Cites Work
- On full abstraction for PCF: I, II and III
- Full abstraction for PCF
- State-dependent representation independence
- A complete, co-inductive syntactic theory of sequential control and state
- Title not available (Why is that?)
- Operational reasoning for functions with local state
- A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References
- Small bisimulations for reasoning about higher-order imperative programs
- Fully abstract models of typed \(\lambda\)-calculi
- A complete normal-form bisimilarity for state
- The marriage of bisimulations and Kripke logical relations
- Logical Bisimulations and Functional Languages
- A fully abstract may testing semantics for concurrent objects
- Reasoning about functions with effects
- Typed Normal Form Bisimulation
- A variable typed logic of effects
- A System-Level Game Semantics
- Title not available (Why is that?)
- Kripke Open Bisimulation
- Transition systems over games
- Title not available (Why is that?)
- Trace semantics for polymorphic references
- A Fully Abstract Trace Semantics for General References
- Environmental Bisimulations for Delimited-Control Operators
- Operational Nominal Game Semantics
- The impact of higher-order state and control effects on local relational reasoning
- A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc
- Open Bisimulation for Aspects
Cited In (3)
This page was built for publication: Complete trace models of state and control
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233464)
