Program equivalence in a simple language with state

DOI10.1016/j.cl.2012.02.002zbMath1248.68155OpenAlexW2067169385MaRDI QIDQ456473

Nikos Tzevelekos

Publication date: 25 October 2012

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2012.02.002

zbMATH Keywords

game semanticslogical relationsenvironmental bisimulationshigher-order computation and local statenominal computationprogram equivalence

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Denotational Semantics with Nominal Scott Domains

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Notions of computation and monads
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• A theory of bisimulation for a fragment of concurrent ML with local names
• Kripke logical relations and PCF
• Game-theoretic analysis of call-by-value computation
• A game semantics of names and pointers
• Algorithmic Nominal Game Semantics
• Introduction to Categories and Categorical Logic
• A Fragment of ML Decidable by Visibly Pushdown Automata
• Full abstraction for nominal general references
• Logical relations for monadic types
• A bisimulation for type abstraction and recursion
• Realisability semantics of parametric polymorphism, general references and recursive types
• Full Abstraction for Reduced ML
• The impact of higher-order state and control effects on local relational reasoning
• State-dependent representation independence
• Finite state machines for strings over infinite alphabets
• Computer Science Logic
• Foundations of Software Science and Computation Structures
• Small bisimulations for reasoning about higher-order imperative programs
• Game Semantics for Higher-Order Concurrency
• Fresh-register automata
• Intensional interpretations of functionals of finite type I
• From Applicative to Environmental Bisimulation
• Untyped lambda-calculus with input-output
• Programming Languages and Systems
• A bisimulation for dynamic sealing
• Finitary PCF is not decidable

This page was built for publication: Program equivalence in a simple language with state