Fully abstract normal form bisimulation for call-by-value PCF

DOI10.1145/3765737MaRDI QIDQ6869433zbMATH OpenFDO

Authors Vasileios Koutavas, Yu-Yang Lin, Nikos Tzevelekos

Publication date 22 January 2026

Published in Journal of the ACM (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

bounded program equivalence verificationcall-by-value PCFcontextual equivalencefull abstractiongame semanticslabelled transition systemsnormal-form bisimulationoperational semantics

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• A bisimulation for dynamic sealing
• A bisimulation for type abstraction and recursion
• A complete normal-form bisimilarity for state
• A complete, co-inductive syntactic theory of sequential control and state
• A Fully Abstract Trace Semantics for General References
• A system-level game semantics
• Enhancements of the bisimulation proof method
• Finitary PCF is not decidable
• From applicative to environmental bisimulation
• From bounded checking to verification of equivalence via symbolic up-to techniques
• Full abstraction for nominal general references
• Full abstraction for PCF
• Fully abstract models of typed \(\lambda\)-calculi
• Game-theoretic analysis of call-by-value computation
• scientific article; zbMATH DE number 1223609 (Why is no real title available?)
• scientific article; zbMATH DE number 1259144 (Why is no real title available?)
• scientific article; zbMATH DE number 1330448 (Why is no real title available?)
• scientific article; zbMATH DE number 1499102 (Why is no real title available?)
• Kripke logical relations and PCF
• LCF considered as a programming language
• Nominal sets. Names and symmetry in computer science
• Normal form bisimulations for delimited-control operators
• Normal form simulation for McCarthy's \textsf{amb}
• On full abstraction for PCF: I, II and III
• Open Bisimulation for Aspects
• Operational nominal game semantics
• Programming Languages and Systems
• Proving congruence of bisimulation in functional programming languages
• Small bisimulations for reasoning about higher-order imperative programs
• The lazy lambda calculus in a concurrency scenario
• Typed Normal Form Bisimulation

This page was built for publication: Fully abstract normal form bisimulation for call-by-value PCF

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