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

sortingtheorem provingalgorithm synthesis

Mathematics Subject Classification ID

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

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)

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

Describes a project that uses

Uses Software

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

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)