Proving properties of functional programs by equality saturation

DOI10.1134/S0361768815030056zbMATH Open1339.68040MaRDI QIDQ300342FDOQ300342

Authors: S. A. Grechanik 

Publication date: 27 June 2016

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

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

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

Cited In (3)

• Title not available (Why is that?)
• Inductive prover based on equality saturation for a lazy functional language
• An algorithm deciding functional equivalence in a new class of program schemes

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)