Proving soundness of extensional normal-form bisimilarities
From MaRDI portal
Publication:2130582
DOI10.1016/j.entcs.2018.03.015WikidataQ113317565 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
congruence; \(\lambda\)-calculus; control operators; \(\eta\)-expansion; bisimulation up to context; normal-form bisimulations
68Q55: Semantics in the theory of computing
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Uses Software
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