Small bisimulations for reasoning about higher-order imperative programs
From MaRDI portal
Publication:5348920
DOI10.1145/1111037.1111050zbMath1370.68048OpenAlexW2125379835MaRDI QIDQ5348920
Mitchell Wand, Vasileios Koutavas
Publication date: 21 August 2017
Published in: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1111037.1111050
Related Items (22)
New ⋮ 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 ⋮ Algorithmic games for full ground references ⋮ A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation ⋮ Refactoring and representation independence for class hierarchies ⋮ Reasoning about multi-stage programs ⋮ First-order reasoning for higher-order concurrency ⋮ Program equivalence in a simple language with state ⋮ Modular Verification of Procedure Equivalence in the Presence of Memory Allocation ⋮ Complete trace models of state and control ⋮ From Applicative to Environmental Bisimulation ⋮ Bisimulation and coinduction enhancements: a historical perspective ⋮ Linearity and bisimulation ⋮ Towards `up to context' reasoning about higher-order processes ⋮ Equations, Contractions, and Unique Solutions ⋮ (Bi)simulations up-to characterise process semantics ⋮ Unnamed Item ⋮ Full Abstraction at Package Boundaries of Object-Oriented Languages ⋮ A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References ⋮ Unnamed Item ⋮ Unnamed Item
This page was built for publication: Small bisimulations for reasoning about higher-order imperative programs
