Program equivalence in linear contexts
From MaRDI portal
Publication:2346993
Abstract: Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at contextual equivalence in the usual (non-linear) functional languages, and fail in capturing non-trivial equivalent programs in linear contexts, particularly when non-determinism is present. We propose the notion of linear contextual equivalence to formally characterize such program equivalence, as well as a novel and general approach to studying it in higher-order languages, based on labeled transition systems specifically designed for functional languages. We show that linear contextual equivalence indeed coincides with trace equivalence - it is sound and complete. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggi's framework) functional languages.
Recommendations
Cites work
- scientific article; zbMATH DE number 4039251 (Why is no real title available?)
- scientific article; zbMATH DE number 1223609 (Why is no real title available?)
- scientific article; zbMATH DE number 1241702 (Why is no real title available?)
- scientific article; zbMATH DE number 2238212 (Why is no real title available?)
- A Calculus for Game-Based Security Proofs
- A Marriage of Rely/Guarantee and Separation Logic
- A fully abstract semantics for a higher-order functional language with nondeterministic computation
- A linear logical framework
- A type system for bounded space and functional in-place update
- Completeness of bisimilarity for contextual equivalence in linear theories
- Foundations of Cryptography
- Foundations of Cryptography
- LCF considered as a programming language
- Linear types and non-size-increasing polynomial time computation.
- Linearity and bisimulation
- Local rely-guarantee reasoning
- Logical relations and the typed λ-calculus
- Logical relations for monadic types
- Notions of computation and monads
- On full abstraction for PCF: I, II and III
- On regions and linear types (extended abstract)
- Operational properties of \texttt{Lily}, a polymorphic linear lambda calculus with recursion
- Parametric polymorphism and operational equivalence
- Program equivalence in a linear functional language
- Proving congruence of bisimulation in functional programming languages
- The Rely-Guarantee method for verifying shared variable concurrent programs
- The computational SLR: a logic for reasoning about computational indistinguishability
Cited in
(8)- A contextual equivalence checker for IMJ*
- Programming Languages and Systems
- Program equivalence in a simple language with state
- Algorithm to find invariant linear inequality constraints in programs
- Algorithm for verifying the equivalence of linear unary recursive programs on ordered semigroup scales
- Reconstruction of linear index expressions for reducing programs to a linear class
- An algorithm deciding functional equivalence in a new class of program schemes
- Equivalence Checking of Non-deterministic Operations
This page was built for publication: Program equivalence in linear contexts
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2346993)
