Proving soundness of extensional normal-form bisimilarities

DOI10.23638/LMCS-15(1:31)2019MaRDI QIDQ5376646zbMATH OpenFDO

Authors Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk

Publication date 17 May 2019

Full work available at URL https://arxiv.org/abs/1711.00113

zbMATH Keywords

contextual equivalencedelimited continuationnormal-form bisimulationup-to technique

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Normal form bisimulations for delimited-control operators
• A sound and complete bisimulation for contextual equivalence in -calculus with call/cc
• Typed Normal Form Bisimulation
• Bisimulations for delimited-control operators
• Applicative bisimulations for delimited-control operators

Cited in

(9)

• Proving soundness of extensional normal-form bisimilarities
• Towards `up to context' reasoning about higher-order processes
• Normal form bisimulations for delimited-control operators
• A sound and complete bisimulation for contextual equivalence in -calculus with call/cc
• Typed Normal Form Bisimulation
• Bisimulations for delimited-control operators
• Effectful normal form bisimulation
• A complete normal-form bisimilarity for algebraic effects and handlers
• Meaningfulness and genericity in a subsuming framework (invited talk)

Describes a project that uses

Uses Software

• Coq

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

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