Proof-based synthesis of sorting algorithms for trees

DOI10.1007/978-3-319-30000-9_43MaRDI QIDQ2798749zbMATH OpenOpenAlexFDO

Authors Isabela Drămnesc, Tudor Jebelean, Sorin Stratulat

Publication date 13 April 2016

Published in Language and Automata Theory and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-30000-9_43

zbMATH Keywords

algorithm synthesissortingtheorem proving

Mathematics Subject Classification ID

Searching and sorting (68P10) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Nonnumerical algorithms (68W05)

Recommendations

• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Synthesis of list algorithms by mechanical proving
• Synthesis of sorting algorithms using multisets in \textit{Theorema}
• Deductive synthesis of sorting programs
• From program verification to program synthesis

Cited in

(8)

• Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
• Deductive synthesis of sorting programs
• Synthesis of sorting algorithms using multisets in \textit{Theorema}
• Recursive proofs for inductive tree data-structures
• scientific article; zbMATH DE number 3917747 (Why is no real title available?)
• Synthesis of list algorithms by mechanical proving
• Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• Mathematica
• Theorema
• Fiat
• Coq
• Isabelle/HOL

This page was built for publication: Proof-based synthesis of sorting algorithms for trees

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