Equivalence in functional languages with effects

DOI10.1017/S0956796800000125zbMath0941.68540OpenAlexW1973030866MaRDI QIDQ4939702

Ian A. Mason, Carolyn L. Talcott

Publication date: 9 February 2000

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796800000125

zbMATH Keywords

equational theorycall-by-value lambda claculusfunctional languages with storeobjects with memory

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Related Items (24)

Semantics of value recursion for Monadic Input/Output ⋮ A categorical interpretation of Landin's correspondence principle ⋮ The impact of higher-order state and control effects on local relational reasoning ⋮ On bisimilarity in lambda calculi with continuous probabilistic choice ⋮ 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 ⋮ An observationally complete program logic for imperative higher-order functions ⋮ A first order logic of effects ⋮ Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec ⋮ Program equivalence in an untyped, call-by-value functional language with uncurried functions ⋮ Reasoning about multi-stage programs ⋮ Local variable scoping and Kleene algebra with tests ⋮ Effectful applicative similarity for call-by-name lambda calculi ⋮ Inferring the equivalence of functional programs that mutate data ⋮ A theory of binding structures and applications to rewriting ⋮ On generic context lemmas for higher-order calculi with sharing ⋮ Operational Properties of Lily, a Polymorphic Linear Lambda Calculus with Recursion ⋮ Capsules and Closures ⋮ From Applicative to Environmental Bisimulation ⋮ Unnamed Item ⋮ A case study in programming coinductive proofs: Howe’s method ⋮ On a monadic semantics for freshness ⋮ Contextual equivalence for inductive definitions with binders in higher order typed functional programming

Uses Software

• ABCL

Cites Work

• Verification of programs that destructively manipulated data
• The lambda calculus, its syntax and semantics
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Side effects and aliasing can have simple axiomatic descriptions
• Fast Decision Procedures Based on Congruence Closure
• Reasoning About Recursively Defined Data Structures
• The Mechanical Evaluation of Expressions

This page was built for publication: Equivalence in functional languages with effects