diff --git a/web/entries/Closest_Pair_Points.html b/web/entries/Closest_Pair_Points.html --- a/web/entries/Closest_Pair_Points.html +++ b/web/entries/Closest_Pair_Points.html @@ -1,181 +1,185 @@ Closest Pair of Points Algorithms - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Closest Pair of Points Algorithms

 

+ + + + - +
Title: Closest Pair of Points Algorithms
Authors: Martin Rau (martin /dot/ rau /at/ tum /dot/ de) and Tobias Nipkow
Submission date: 2020-01-13
Abstract: This entry provides two related verified divide-and-conquer algorithms solving the fundamental Closest Pair of Points problem in Computational Geometry. Functional correctness and the optimal running time of O(n log n) are proved. Executable code is generated which is empirically competitive with handwritten reference implementations.
Change history:[2020-14-04]: Incorporate Time_Monad of the AFP entry Root_Balanced_Tree.
BibTeX: 
@article{Closest_Pair_Points-AFP,
   author  = {Martin Rau and Tobias Nipkow},
   title   = {Closest Pair of Points Algorithms},
   journal = {Archive of Formal Proofs},
   month   = jan,
   year    = 2020,
   note    = {\url{http://isa-afp.org/entries/Closest_Pair_Points.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Akra_Bazzi
Akra_Bazzi, Root_Balanced_Tree

Proof outline
Proof document
Browse theories
Download this entry
Older releases: None
\ No newline at end of file diff --git a/web/entries/KD_Tree.html b/web/entries/KD_Tree.html --- a/web/entries/KD_Tree.html +++ b/web/entries/KD_Tree.html @@ -1,187 +1,193 @@ Multidimensional Binary Search Trees - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Multidimensional Binary Search Trees

 

+ + + +
Title: Multidimensional Binary Search Trees
Author: Martin Rau (martin /dot/ rau /at/ tum /dot/ de)
Submission date: 2019-05-30
Abstract: This entry provides a formalization of multidimensional binary trees, also known as k-d trees. It includes a balanced build algorithm as well as the nearest neighbor algorithm and the range search algorithm. It is based on the papers Multidimensional binary search trees used for associative searching and An Algorithm for Finding Best Matches in Logarithmic Expected Time.
Change history:[2020-15-04]: Change representation of k-dimensional points from 'list' to +HOL-Analysis.Finite_Cartesian_Product 'vec'. Update proofs +to incorporate HOL-Analysis 'dist' and 'cbox' primitives.
BibTeX: 
@article{KD_Tree-AFP,
   author  = {Martin Rau},
   title   = {Multidimensional Binary Search Trees},
   journal = {Archive of Formal Proofs},
   month   = may,
   year    = 2019,
   note    = {\url{http://isa-afp.org/entries/KD_Tree.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Median_Of_Medians_Selection

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Lambda_Free_RPOs.html b/web/entries/Lambda_Free_RPOs.html --- a/web/entries/Lambda_Free_RPOs.html +++ b/web/entries/Lambda_Free_RPOs.html @@ -1,200 +1,202 @@ Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms

 

- + + +
Title: Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
Authors: Jasmin Christian Blanchette (j /dot/ c /dot/ blanchette /at/ vu /dot/ nl), Uwe Waldmann (uwe /at/ mpi-inf /dot/ mpg /dot/ de) and Daniel Wand (dwand /at/ mpi-inf /dot/ mpg /dot/ de)
Submission date: 2016-09-23
Abstract: This Isabelle/HOL formalization defines recursive path orders (RPOs) for higher-order terms without lambda-abstraction and proves many useful properties about them. The main order fully coincides with the standard RPO on first-order terms also in the presence of currying, distinguishing it from previous work. An optimized variant is formalized as well. It appears promising as the basis of a higher-order superposition calculus.
BibTeX: 
@article{Lambda_Free_RPOs-AFP,
   author  = {Jasmin Christian Blanchette and Uwe Waldmann and Daniel Wand},
   title   = {Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms},
   journal = {Archive of Formal Proofs},
   month   = sep,
   year    = 2016,
   note    = {\url{http://isa-afp.org/entries/Lambda_Free_RPOs.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on:Nested_Multisets_Ordinals
Used by: Higher_Order_Terms, Lambda_Free_EPO, Lambda_Free_KBOs

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Nested_Multisets_Ordinals.html b/web/entries/Nested_Multisets_Ordinals.html --- a/web/entries/Nested_Multisets_Ordinals.html +++ b/web/entries/Nested_Multisets_Ordinals.html @@ -1,202 +1,202 @@ Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

 

- +
Title: Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
Authors: Jasmin Christian Blanchette (j /dot/ c /dot/ blanchette /at/ vu /dot/ nl), Mathias Fleury (fleury /at/ mpi-inf /dot/ mpg /dot/ de) and Dmitriy Traytel
Submission date: 2016-11-12
Abstract: This Isabelle/HOL formalization introduces a nested multiset datatype and defines Dershowitz and Manna's nested multiset order. The order is proved well founded and linear. By removing one constructor, we transform the nested multisets into hereditary multisets. These are isomorphic to the syntactic ordinals—the ordinals can be recursively expressed in Cantor normal form. Addition, subtraction, multiplication, and linear orders are provided on this type.
BibTeX: 
@article{Nested_Multisets_Ordinals-AFP,
   author  = {Jasmin Christian Blanchette and Mathias Fleury and Dmitriy Traytel},
   title   = {Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals},
   journal = {Archive of Formal Proofs},
   month   = nov,
   year    = 2016,
   note    = {\url{http://isa-afp.org/entries/Nested_Multisets_Ordinals.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: List-Index, Ordinal
Used by:Functional_Ordered_Resolution_Prover, Lambda_Free_KBOs, Ordered_Resolution_Prover
Functional_Ordered_Resolution_Prover, Lambda_Free_KBOs, Lambda_Free_RPOs, Ordered_Resolution_Prover

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/entries/Root_Balanced_Tree.html b/web/entries/Root_Balanced_Tree.html --- a/web/entries/Root_Balanced_Tree.html +++ b/web/entries/Root_Balanced_Tree.html @@ -1,202 +1,202 @@ Root-Balanced Tree - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Root-Balanced Tree

 

- +
Title: Root-Balanced Tree
Author: Tobias Nipkow
Submission date: 2017-08-20
Abstract:

Andersson introduced general balanced trees, search trees based on the design principle of partial rebuilding: perform update operations naively until the tree becomes too unbalanced, at which point a whole subtree is rebalanced. This article defines and analyzes a functional version of general balanced trees, which we call root-balanced trees. Using a lightweight model of execution time, amortized logarithmic complexity is verified in the theorem prover Isabelle.

This is the Isabelle formalization of the material decribed in the APLAS 2017 article Verified Root-Balanced Trees by the same author, which also presents experimental results that show competitiveness of root-balanced with AVL and red-black trees.

BibTeX: 
@article{Root_Balanced_Tree-AFP,
   author  = {Tobias Nipkow},
   title   = {Root-Balanced Tree},
   journal = {Archive of Formal Proofs},
   month   = aug,
   year    = 2017,
   note    = {\url{http://isa-afp.org/entries/Root_Balanced_Tree.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Amortized_Complexity
Used by:CakeML_Codegen
CakeML_Codegen, Closest_Pair_Points

Proof outline
Proof document
Browse theories
Download this entry
Older releases:
\ No newline at end of file diff --git a/web/statistics.html b/web/statistics.html --- a/web/statistics.html +++ b/web/statistics.html @@ -1,303 +1,303 @@ Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

Statistics

 

Statistics

Number of Articles:527
Number of Authors:347
Number of lemmas:~143,000
Lines of Code:~2,483,100

Most used AFP articles:

NameUsed by ? articles
1. List-Index 14
2. Coinductive 12
Collections 12
Regular-Sets 12
3. Landau_Symbols 11
4. Show 10
5. Abstract-Rewriting 9
Automatic_Refinement 9
Deriving 9
6. Jordan_Normal_Form 8
Native_Word 8

Growth in number of articles:

Growth in lines of code:

Growth in number of authors:

Size of articles:
\ No newline at end of file