Proving soundness of extensional normal-form bisimilarities

DOI10.1016/J.ENTCS.2018.03.015OpenAlexW2767024947WikidataQ113317565 ScholiaQ113317565MaRDI QIDQ2130582

Piotr Polesiuk, Dariusz Biernacki, Sergueï Lenglet

Publication date: 25 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.03.015

zbMATH Keywords

congruence\(\lambda\)-calculuscontrol operators\(\eta\)-expansionbisimulation up to contextnormal-form bisimulations

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Diacritical companions

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Full abstraction in the lazy lambda calculus
• Axioms for control operators in the CPS hierarchy
• Normal Form Bisimulations for Delimited-Control Operators
• A complete, co-inductive syntactic theory of sequential control and state
• Bisimulations Up-to: Beyond First-Order Transition Systems
• Typed Normal Form Bisimulation
• Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
• Enhancements of the bisimulation proof method

This page was built for publication: Proving soundness of extensional normal-form bisimilarities