Inferring the equivalence of functional programs that mutate data

DOI10.1016/0304-3975(92)90301-UzbMath0768.68092MaRDI QIDQ1196301

Ian A. Mason, Carolyn L. Talcott

Publication date: 16 December 1992

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

formal systeminductionconstrained equivalence of programs with effectssingle- conclusion consequence relation

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items

A categorical interpretation of Landin's correspondence principle, A first order logic of effects, A theory of binding structures and applications to rewriting, Unnamed Item

Cites Work

• Verification of programs that destructively manipulated data
• The revised report on the syntactic theories of sequential control and state
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Model theory
• Solvable cases of the decision problem
• Side effects and aliasing can have simple axiomatic descriptions
• Fast Decision Procedures Based on Congruence Closure
• Reasoning About Recursively Defined Data Structures
• Equivalence in functional languages with effects
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item