Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (Q1640636): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HipSpec
@@ Property / describes a project that uses: HipSpec / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Easychair
@@ Property / describes a project that uses: Easychair / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.jsc.2018.04.002
+Normal rank
@@ Property / OpenAlex ID @@
+W2805273157
@@ Property / OpenAlex ID: W2805273157 / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement Calculus
@@ Property / cites work: Refinement Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754027
@@ Property / cites work: Q2754027 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484330
@@ Property / cites work: Q4484330 / rank @@
+Normal rank
@@ Property / cites work @@
+Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+Program Development in Computational Logic
@@ Property / cites work: Program Development in Computational Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q4780208
@@ Property / cites work: Q4780208 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5699466
@@ Property / cites work: Q5699466 / rank @@
+Normal rank
@@ Property / cites work @@
+Artificial Intelligence and Symbolic Computation
@@ Property / cites work: Artificial Intelligence and Symbolic Computation / rank @@
+Normal rank
@@ Property / cites work @@
+Q2847391
@@ Property / cites work: Q2847391 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorema 2.0: Computer-Assisted Natural-Style Mathematics
+Normal rank
@@ Property / cites work @@
+Automating Inductive Proofs Using Theory Exploration
+Normal rank
@@ Property / cites work @@
+Refinements for Free!
@@ Property / cites work: Refinements for Free! / rank @@
+Normal rank
@@ Property / cites work @@
+Fiat
@@ Property / cites work: Fiat / rank @@
+Normal rank
@@ Property / cites work @@
+Logic program synthesis
@@ Property / cites work: Logic program synthesis / rank @@
+Normal rank
@@ Property / cites work @@
+Synthesis of list algorithms by mechanical proving
+Normal rank
@@ Property / cites work @@
+Proof–Based Synthesis of Sorting Algorithms for Trees
+Normal rank
@@ Property / cites work @@
+Q4707743
@@ Property / cites work: Q4707743 / rank @@
+Normal rank
@@ Property / cites work @@
+Conjecture synthesis for inductive theories
@@ Property / cites work: Conjecture synthesis for inductive theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q4349924
@@ Property / cites work: Q4349924 / rank @@
+Normal rank
@@ Property / cites work @@
+Linear resolution with selection function
@@ Property / cites work: Linear resolution with selection function / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Mechanically certifying formula-based Noetherian induction reasoning
+Normal rank
@@ Property / cites work @@
+Program development by stepwise refinement
@@ Property / cites work: Program development by stepwise refinement / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q129701038
@@ Property / Wikidata QID: Q129701038 / rank @@
+Normal rank