Observational program calculi and the correctness of translations
From MaRDI portal
Publication:2339472
DOI10.1016/j.tcs.2015.02.027zbMath1309.68052OpenAlexW2162146115MaRDI QIDQ2339472
David Sabel, Jan Schwinghammer, Manfred Schmidt-Schauss, Joachim Niehren
Publication date: 1 April 2015
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2015.02.027
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Unnamed Item ⋮ Observing Success in the Pi-Calculus ⋮ On generic context lemmas for higher-order calculi with sharing
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A two-valued logic for properties of strict functional programs allowing partial functions
- The lambda calculus. Its syntax and semantics. Rev. ed.
- A concurrent lambda calculus with futures
- On generic context lemmas for higher-order calculi with sharing
- Closures of may-, should- and must-convergences for contextual equivalence
- On the expressive power of programming languages
- LCF considered as a programming language
- Fully abstract models of typed \(\lambda\)-calculi
- Full abstraction in the lazy lambda calculus
- On abstraction and the expressive power of programming languages
- Testing equivalences for processes
- Formal foundations of operational semantics
- Bisimilarity as a theory of functional programming
- On the representation of McCarthy's \(amb\) in the \(\pi\)-calculus
- Proving congruence of bisimulation in functional programming languages
- From operational semantics to domain theory
- Correctness of Program Transformations as a Termination Problem
- Fully abstract compilation to JavaScript
- Biorthogonality, step-indexing and compiler correctness
- The marriage of bisimulations and Kripke logical relations
- Extending Abramsky's lazy lambda calculus: (non)-conservativity of embeddings
- Conservative Concurrency in Haskell
- Branching vs. Linear Time: Semantical Perspective
- A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations
- Parametric polymorphism and operational equivalence
- Full Abstraction and the Context Lemma
- An equivalence-preserving CPS translation via multi-language semantics
- Typed closure conversion preserves observational equivalence
- Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq
- Correctness of an STM Haskell implementation
- A verified compiler for an impure functional language
- State-dependent representation independence
- Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures
- A bisimulation for type abstraction and recursion
- A non-deterministic call-by-need lambda calculus
- Simulation in the call-by-need lambda-calculus with letrec
- A kripke logical relation between ML and assembly
- Howe's method for higher-order languages
- Programming Languages and Systems
