A Fully Abstract Trace Semantics for General References

DOI10.1007/978-3-540-73420-8_58MaRDI QIDQ5428848zbMATH OpenOpenAlexFDO

Authors James Laird

Publication date 28 November 2007

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73420-8_58

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Trace semantics for polymorphic references
• Operational nominal game semantics
• Complete trace models of state and control
• Full abstraction for nominal general references
• Deconstructing general references via game semantics

Cited in

(23)

• A curry-style semantics of interaction: from untyped to second-order lazy -calculus
• Complete trace models of state and control
• Higher-order linearisability
• Operational nominal game semantics
• A system-level game semantics
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• Trace Semantics for IPDL
• Realisability semantics of parametric polymorphism, general references and recursive types
• A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References
• scientific article; zbMATH DE number 1949638 (Why is no real title available?)
• Trace semantics for polymorphic references
• Deconstructing general references via game semantics
• Higher-order linearisability
• Global state considered helpful
• Full Abstraction for Linda
• From applicative to environmental bisimulation
• Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts
• From bounded checking to verification of equivalence via symbolic up-to techniques
• Symbolic execution game semantics
• Fully abstract normal form bisimulation for call-by-value PCF
• Pushdown normal-form bisimulation: a nominal context-free approach to program equivalence
• First-order store and visibility in name-passing calculi
• Nanopass back-translation of call-return trees for mechanized secure compilation proofs

This page was built for publication: A Fully Abstract Trace Semantics for General References

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