A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc

DOI10.1007/978-3-319-47958-3_10zbMath1483.68064OpenAlexW2527872993MaRDI QIDQ3179291

Eijiro Sumii, Taichi Yachi

Publication date: 21 December 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-47958-3_10

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (2)

Complete trace models of state and control ⋮ Unnamed Item

Cites Work

• A syntactic theory of sequential control
• The revised report on the syntactic theories of sequential control and state
• Normal Form Bisimulations for Delimited-Control Operators
• Environmental Bisimulations for Delimited-Control Operators
• The marriage of bisimulations and Kripke logical relations
• The impact of higher-order state and control effects on local relational reasoning
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• A bisimulation for type abstraction and recursion
• A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References
• A sound and complete axiomatization of delimited continuations
• A bisimulation for type abstraction and recursion
• Small bisimulations for reasoning about higher-order imperative programs
• Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation
• A bisimulation for dynamic sealing

This page was built for publication: A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc