Algorithmic games for full ground references

DOI10.1007/s10703-017-0292-9zbMath1392.68147WikidataQ59613817 ScholiaQ59613817MaRDI QIDQ1650867

Nikos Tzevelekos, Andrzej S. Murawski

Publication date: 16 July 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0292-9

zbMATH Keywords

full abstraction; game semantics; program equivalence; automata over infinite alphabets

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68N15: Theory of programming languages

68Q55: Semantics in the theory of computing

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Operationally-based program equivalence proofs using LCTRSs, Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts, On-the-fly bisimilarity checking for fresh-register automata

Uses Software

• eVolCheck
• SymDiff
• coneqct

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Functions with local state: regularity and undecidability
• A new approach to abstract syntax with variable binding
• Context-free languages over infinite alphabets
• Correctness of data representations involving heap data structures
• Game-theoretic analysis of call-by-value computation
• A game semantics of names and pointers
• Regression Verification for Multi-threaded Programs
• Fragments of ML Decidable by Nested Data Class Memory Automata
• Algorithmic Nominal Game Semantics
• A Fragment of ML Decidable by Visibly Pushdown Automata
• Algorithmic Games for Full Ground References
• Full abstraction for nominal general references
• A Contextual Equivalence Checker for IMJ*
• Game Semantic Analysis of Equivalence in IMJ
• Visibly pushdown languages
• Full Abstraction for Reduced ML
• Deconstructing General References via Game Semantics
• The impact of higher-order state and control effects on local relational reasoning
• State-dependent representation independence
• eVolCheck: Incremental Upgrade Checker for C
• Small bisimulations for reasoning about higher-order imperative programs
• Typed Lambda Calculi and Applications