A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References

DOI10.1007/978-3-642-04027-6_33zbMath1257.03040OpenAlexW1847926715MaRDI QIDQ3644766

Eijiro Sumii

Publication date: 12 November 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04027-6_33

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (6)

A Sound and Complete Bisimulation for Contextual Equivalence in $$\lambda $$ -Calculus with Call/cc ⋮ A Complete, Co-inductive Syntactic Theory of Sequential Control and State ⋮ A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation ⋮ Refactoring and representation independence for class hierarchies ⋮ Complete trace models of state and control ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• A complete, co-inductive syntactic theory of sequential control and state
• A bisimulation for type abstraction and recursion
• A Theory of Non-monotone Memory (Or: Contexts for free)
• Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
• State-dependent representation independence
• Small bisimulations for reasoning about higher-order imperative programs
• Relational Reasoning for Recursive Types and References
• A Fully Abstract Trace Semantics for General References
• Behavioral equivalence in the polymorphic pi-calculus
• A bisimulation for dynamic sealing

This page was built for publication: A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References