Proving properties of functional programs by equality saturation

DOI10.1134/S0361768815030056zbMath1339.68040MaRDI QIDQ300342

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)

Uses Software

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

Cites Work

• A predicative analysis of structural recursion
• Zeno: An Automated Prover for Properties of Recursive Data Structures
• 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
• Fast Decision Procedures Based on Congruence Closure
• A positive supercompiler
• Automating Inductive Proofs Using Theory Exploration
• Equality saturation

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