Inferring the equivalence of functional programs that mutate data

DOI10.1016/0304-3975(92)90301-UMaRDI QIDQ1196301zbMATH OpenFDO

Authors Ian A. Mason, Carolyn Talcott

Publication date 16 December 1992

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

zbMATH Keywords

inductionformal systemconstrained equivalence of programs with effectssingle- conclusion consequence relation

Mathematics Subject Classification ID

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

Recommendations

• Verification of programs that destructively manipulated data
• scientific article; zbMATH DE number 4189708
• Equivalence checking of two functional programs using inductive theorem provers
• Inference rules for proving the equivalence of recursive procedures
• Inference rules for proving the equivalence of recursive procedures

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 3864473 (Why is no real title available?)
• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• scientific article; zbMATH DE number 43015 (Why is no real title available?)
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Equivalence in functional languages with effects
• Fast Decision Procedures Based on Congruence Closure
• Model theory
• Reasoning About Recursively Defined Data Structures
• Side effects and aliasing can have simple axiomatic descriptions
• Solvable cases of the decision problem
• The revised report on the syntactic theories of sequential control and state
• Verification of programs that destructively manipulated data

Cited in

(8)

• Equivalence checking of two functional programs using inductive theorem provers
• A theory of binding structures and applications to rewriting
• A first order logic of effects
• Program equivalence in a typed probabilistic call-by-need functional language
• Inferring functional properties of matrix manipulating programs by abstract interpretation
• scientific article; zbMATH DE number 4189708 (Why is no real title available?)
• A categorical interpretation of Landin's correspondence principle
• scientific article; zbMATH DE number 7056232 (Why is no real title available?)

This page was built for publication: Inferring the equivalence of functional programs that mutate data

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1196301)