Program equivalence in linear contexts
From MaRDI portal
Publication:2346993
DOI10.1016/J.TCS.2015.03.006zbMATH Open1327.68078arXiv1106.2872OpenAlexW2129096339MaRDI QIDQ2346993FDOQ2346993
Authors: Yu Zhang, Yuxin Deng 
Publication date: 26 May 2015
Published in: Theoretical Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1106.2872
Recommendations
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)
Cites Work
- LCF considered as a programming language
- On full abstraction for PCF: I, II and III
- Title not available (Why is that?)
- Notions of computation and monads
- Linear types and non-size-increasing polynomial time computation.
- Foundations of Cryptography
- Foundations of Cryptography
- Proving congruence of bisimulation in functional programming languages
- Logical relations and the typed λ-calculus
- Title not available (Why is that?)
- A Marriage of Rely/Guarantee and Separation Logic
- Title not available (Why is that?)
- On regions and linear types (extended abstract)
- The Rely-Guarantee method for verifying shared variable concurrent programs
- Completeness of bisimilarity for contextual equivalence in linear theories
- A linear logical framework
- Title not available (Why is that?)
- Logical relations for monadic types
- Linearity and bisimulation
- A type system for bounded space and functional in-place update
- Local rely-guarantee reasoning
- Parametric polymorphism and operational equivalence
- A fully abstract semantics for a higher-order functional language with nondeterministic computation
- Operational properties of \texttt{Lily}, a polymorphic linear lambda calculus with recursion
- A Calculus for Game-Based Security Proofs
- The computational SLR: a logic for reasoning about computational indistinguishability
- Program equivalence in a linear functional language
Cited In (8)
- 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
- Equivalence Checking of Non-deterministic Operations
- An algorithm deciding functional equivalence in a new class of program schemes
- A contextual equivalence checker for IMJ*
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)
