The marriage of bisimulations and Kripke logical relations

DOI10.1145/2103656.2103666zbMath1321.68198OpenAlexW4239690658MaRDI QIDQ2942857

Georg Neis, Viktor Vafeiadis, Derek R. Dreyer, Chung-Kil Hur

Publication date: 11 September 2015

Published in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2103656.2103666

zbMATH Keywords

transitivitybisimulationscontextual equivalencerecursive typesabstract typesKripke logical relationsglobal vs. local knowledgehigher-order staterelation transition systems

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) 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 (9)

New ⋮ A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc ⋮ Semantic preservation for a type directed translation scheme of Featherweight Go ⋮ Complete trace models of state and control ⋮ A language-independent proof system for full program equivalence ⋮ Fully abstract trace semantics for protected module architectures ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Observational program calculi and the correctness of translations

This page was built for publication: The marriage of bisimulations and Kripke logical relations