Equivalence in functional languages with effects
From MaRDI portal
Cites work
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Fast Decision Procedures Based on Congruence Closure
- Reasoning About Recursively Defined Data Structures
- Side effects and aliasing can have simple axiomatic descriptions
- The Mechanical Evaluation of Expressions
- The lambda calculus, its syntax and semantics
- Verification of programs that destructively manipulated data
Cited in
(25)- A theory of binding structures and applications to rewriting
- Effectful applicative similarity for call-by-name lambda calculi
- Pushdown normal-form bisimulation: a nominal context-free approach to program equivalence
- Semantics of value recursion for Monadic Input/Output
- Inferring the equivalence of functional programs that mutate data
- A first order logic of effects
- Operational properties of \texttt{Lily}, a polymorphic linear lambda calculus with recursion
- Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec
- An observationally complete program logic for imperative higher-order functions
- On bisimilarity in lambda calculi with continuous probabilistic choice
- A case study in programming coinductive proofs: Howe's method
- Local variable scoping and Kleene algebra with tests
- The impact of higher-order state and control effects on local relational reasoning
- Capsules and closures
- On a monadic semantics for freshness
- Program equivalence in an untyped, call-by-value functional language with uncurried functions
- From applicative to environmental bisimulation
- A Complete, Co-inductive Syntactic Theory of Sequential Control and State
- Encoding abstract syntax without fresh names
- A two-valued logic for properties of strict functional programs allowing partial functions
- Reasoning about multi-stage programs
- A categorical interpretation of Landin's correspondence principle
- On generic context lemmas for higher-order calculi with sharing
- scientific article; zbMATH DE number 7056232 (Why is no real title available?)
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming
This page was built for publication: Equivalence in functional languages with effects
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4939702)
