Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts

DOI10.1007/978-3-031-30829-1_2OpenAlexW4366503988MaRDI QIDQ6091179

Guilhem Jaber, Daniel Hirschkoff, Enguerrand Prebet

Publication date: 24 November 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-30829-1_2

Mathematics Subject Classification ID

Theory of computing (68Qxx) Theory of software (68Nxx)

Cites Work

• Unnamed Item
• Full abstraction for Reduced ML
• Program equivalence in a simple language with state
• Linear logic
• A new approach to abstract syntax with variable binding
• Algorithmic games for full ground references
• A curry-style semantics of interaction: from untyped to second-order lazy \(\lambda\mu\)-calculus
• Complete trace models of state and control
• On a monadic semantics for freshness
• Algorithmic Nominal Game Semantics
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• Full abstraction for nominal general references
• Typed Normal Form Bisimulation
• On the bisimulation proof method
• Proof-Relevant Logical Relations for Name Generation
• Sequentiality and the CPS Semantics of Fresh Names
• A Fully Abstract Trace Semantics for General References
• Typed Lambda Calculi and Applications

This page was built for publication: Deciding contextual equivalence of \(\nu \)-calculus with effectful contexts