diff --git a/metadata/entries/Approximation_Algorithms.toml b/metadata/entries/Approximation_Algorithms.toml --- a/metadata/entries/Approximation_Algorithms.toml +++ b/metadata/entries/Approximation_Algorithms.toml @@ -1,36 +1,36 @@ title = "Verified Approximation Algorithms" date = 2020-01-16 topics = [ "Computer science/Algorithms/Approximation", ] abstract = """ We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, set cover, independent set, center selection, load balancing, and bin packing. The proofs correct incompletenesses in existing proofs and improve the approximation ratio in one case. A detailed description of our work (excluding center selection) has been published in the proceedings of IJCAR 2020.""" license = "bsd" note = "" [authors] [authors.essmann] email = "essmann_email" [authors.nipkow] -homepage = "nipkow_homepage1" +homepage = "nipkow_homepage" [authors.robillard] homepage = "robillard_homepage" [authors.sulejmani] [contributors] [notify] nipkow = "nipkow_email" [history] [extra] diff --git a/metadata/entries/Closest_Pair_Points.toml b/metadata/entries/Closest_Pair_Points.toml --- a/metadata/entries/Closest_Pair_Points.toml +++ b/metadata/entries/Closest_Pair_Points.toml @@ -1,33 +1,33 @@ title = "Closest Pair of Points Algorithms" date = 2020-01-13 topics = [ "Computer science/Algorithms/Geometry", ] 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.""" license = "bsd" note = "" [authors] [authors.rau] email = "rau_email" [authors.nipkow] -homepage = "nipkow_homepage2" +homepage = "nipkow_homepage" [contributors] [notify] rau = "rau_email" nipkow = "nipkow_email" [history] 2020-04-14 = "Incorporate Time_Monad of the AFP entry Root_Balanced_Tree." [extra] diff --git a/metadata/entries/Hoare_Time.toml b/metadata/entries/Hoare_Time.toml --- a/metadata/entries/Hoare_Time.toml +++ b/metadata/entries/Hoare_Time.toml @@ -1,36 +1,36 @@ title = "Hoare Logics for Time Bounds" date = 2018-02-26 topics = [ "Computer science/Programming languages/Logics", ] abstract = """ We study three different Hoare logics for reasoning about time bounds of imperative programs and formalize them in Isabelle/HOL: a classical Hoare like logic due to Nielson, a logic with potentials due to Carbonneaux et al. and a separation logic following work by Atkey, Chaguérand and Pottier. These logics are formally shown to be sound and complete. Verification condition generators are developed and are shown sound and complete too. We also consider variants of the systems where we abstract from multiplicative constants in the running time bounds, thus supporting a big-O style of reasoning. Finally we compare the expressive power of the three systems.""" license = "bsd" note = "" [authors] [authors.haslbeckm] homepage = "haslbeckm_homepage" [authors.nipkow] -homepage = "nipkow_homepage3" +homepage = "nipkow_homepage" [contributors] [notify] haslbeckm = "haslbeckm_email" [history] [extra] diff --git a/metadata/entries/Monad_Memo_DP.toml b/metadata/entries/Monad_Memo_DP.toml --- a/metadata/entries/Monad_Memo_DP.toml +++ b/metadata/entries/Monad_Memo_DP.toml @@ -1,40 +1,40 @@ title = "Monadification, Memoization and Dynamic Programming" date = 2018-05-22 topics = [ "Computer science/Programming languages/Transformations", "Computer science/Algorithms", "Computer science/Functional programming", ] abstract = """ We present a lightweight framework for the automatic verified (functional or imperative) memoization of recursive functions. Our tool can turn a pure Isabelle/HOL function definition into a monadified version in a state monad or the Imperative HOL heap monad, and prove a correspondence theorem. We provide a variety of memory implementations for the two types of monads. A number of simple techniques allow us to achieve bottom-up computation and space-efficient memoization. The framework’s utility is demonstrated on a number of representative dynamic programming problems. A detailed description of our work can be found in the accompanying paper [2].""" license = "bsd" note = "" [authors] [authors.wimmer] homepage = "wimmer_homepage1" [authors.hu] email = "hu_email" [authors.nipkow] -homepage = "nipkow_homepage4" +homepage = "nipkow_homepage" [contributors] [notify] wimmer = "wimmer_email1" [history] [extra] diff --git a/metadata/entries/Optimal_BST.toml b/metadata/entries/Optimal_BST.toml --- a/metadata/entries/Optimal_BST.toml +++ b/metadata/entries/Optimal_BST.toml @@ -1,31 +1,31 @@ title = "Optimal Binary Search Trees" date = 2018-05-27 topics = [ "Computer science/Algorithms", "Computer science/Data structures", ] abstract = """ This article formalizes recursive algorithms for the construction of optimal binary search trees given fixed access frequencies. We follow Knuth (1971), Yao (1980) and Mehlhorn (1984). The algorithms are memoized with the help of the AFP article Monadification, Memoization and Dynamic Programming, thus yielding dynamic programming algorithms.""" license = "bsd" note = "" [authors] [authors.nipkow] -homepage = "nipkow_homepage3" +homepage = "nipkow_homepage" [authors.somogyi] [contributors] [notify] nipkow = "nipkow_email" [history] [extra] diff --git a/metadata/entries/Treaps.toml b/metadata/entries/Treaps.toml --- a/metadata/entries/Treaps.toml +++ b/metadata/entries/Treaps.toml @@ -1,44 +1,44 @@ title = "Treaps" date = 2018-02-06 topics = [ "Computer science/Data structures", ] abstract = """

A Treap is a binary tree whose nodes contain pairs consisting of some payload and an associated priority. It must have the search-tree property w.r.t. the payloads and the heap property w.r.t. the priorities. Treaps are an interesting data structure that is related to binary search trees (BSTs) in the following way: if one forgets all the priorities of a treap, the resulting BST is exactly the same as if one had inserted the elements into an empty BST in order of ascending priority. This means that a treap behaves like a BST where we can pretend the elements were inserted in a different order from the one in which they were actually inserted.

In particular, by choosing these priorities at random upon insertion of an element, we can pretend that we inserted the elements in random order, so that the shape of the resulting tree is that of a random BST no matter in what order we insert the elements. This is the main result of this formalisation.

""" license = "bsd" note = "" [authors] [authors.haslbeck] homepage = "haslbeck_homepage" [authors.eberl] homepage = "eberl_homepage2" [authors.nipkow] -homepage = "nipkow_homepage3" +homepage = "nipkow_homepage" [contributors] [notify] eberl = "eberl_email" [history] [extra] diff --git a/metadata/entries/Weight_Balanced_Trees.toml b/metadata/entries/Weight_Balanced_Trees.toml --- a/metadata/entries/Weight_Balanced_Trees.toml +++ b/metadata/entries/Weight_Balanced_Trees.toml @@ -1,32 +1,32 @@ title = "Weight-Balanced Trees" date = 2018-03-13 topics = [ "Computer science/Data structures", ] abstract = """ This theory provides a verified implementation of weight-balanced trees following the work of Hirai and Yamamoto who proved that all parameters in a certain range are valid, i.e. guarantee that insertion and deletion preserve weight-balance. Instead of a general theorem we provide parameterized proofs of preservation of the invariant that work for many (all?) valid parameters.""" license = "bsd" note = "" [authors] [authors.nipkow] -homepage = "nipkow_homepage3" +homepage = "nipkow_homepage" [authors.dirix] [contributors] [notify] nipkow = "nipkow_email" [history] [extra]