Proving properties of functional programs by equality saturation

DOI10.1134/S0361768815030056MaRDI QIDQ300342zbMATH OpenFDO

Authors S. A. Grechanik

Publication date 27 June 2016

Published in Programming and Computer Software (Search for Journal in Brave)

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Inductive prover based on equality saturation for a lazy functional language
• Semantic determinism and functional logic program properties
• Proving congruence of bisimulation in functional programming languages
• Proofs by induction in equational theories with constructors
• scientific article; zbMATH DE number 1241702

Cites work

• A positive supercompiler
• A predicative analysis of structural recursion
• Automating Inductive Proofs Using Theory Exploration
• Equality saturation
• Fast Decision Procedures Based on Congruence Closure
• Multi-result supercompilation as branching growth of the penultimate level in metasystem transitions
• Simplify: a theorem prover for program checking
• The concept of a supercompiler
• Zeno: an automated prover for properties of recursive data structures

Cited in

(3)

• An algorithm deciding functional equivalence in a new class of program schemes
• Inductive prover based on equality saturation for a lazy functional language
• scientific article; zbMATH DE number 5677418 (Why is no real title available?)

Describes a project that uses

Uses Software

• SIMPLIFY
• Zeno
• HipSpec
• Graphsc
• QuickSpec
• Refal
• GitHub

This page was built for publication: Proving properties of functional programs by equality saturation

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