Complete trace models of state and control

DOI10.1007/978-3-030-72019-3_13zbMath1473.68037arXiv2101.08491MaRDI QIDQ2233464

Guilhem Jaber, Andrzej S. Murawski

Publication date: 18 October 2021

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

zbMATH Keywords

contextual equivalence; control operators; higher-order references; operational game semantics

Mathematics Subject Classification ID

68N15: Theory of programming languages

68Q55: Semantics in the theory of computing

Related Items

Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts, An algebraic theory for shared-state concurrency

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A fully abstract may testing semantics for concurrent objects
• Fully abstract models of typed \(\lambda\)-calculi
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• A variable typed logic of effects
• A complete normal-form bisimilarity for state
• Environmental Bisimulations for Delimited-Control Operators
• The marriage of bisimulations and Kripke logical relations
• Operational Nominal Game Semantics
• The impact of higher-order state and control effects on local relational reasoning
• A System-Level Game Semantics
• A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc
• A complete, co-inductive syntactic theory of sequential control and state
• Kripke Open Bisimulation
• Logical Bisimulations and Functional Languages
• Typed Normal Form Bisimulation
• Open Bisimulation for Aspects
• A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References
• Transition systems over games
• Trace semantics for polymorphic references
• State-dependent representation independence
• Small bisimulations for reasoning about higher-order imperative programs
• A Fully Abstract Trace Semantics for General References