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
- A Calculus for Game-Based Security Proofs
- A fully abstract semantics for a higher-order functional language with nondeterministic computation
- A linear logical framework
- A Marriage of Rely/Guarantee and Separation Logic
- 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
- 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?)
- 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 computational SLR: a logic for reasoning about computational indistinguishability
- The Rely-Guarantee method for verifying shared variable concurrent programs
Cited in
(8)- Reconstruction of linear index expressions for reducing programs to a linear class
- A contextual equivalence checker for IMJ*
- Algorithm for verifying the equivalence of linear unary recursive programs on ordered semigroup scales
- Algorithm to find invariant linear inequality constraints in programs
- Program equivalence in a simple language with state
- Programming Languages and Systems
- Equivalence Checking of Non-deterministic Operations
- An algorithm deciding functional equivalence in a new class of program schemes
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)
