[2011-04-11] Ondrej Kuncar added delete function
A preliminary version of this work (without pairing heaps) is described in a paper published in the proceedings of the conference on Interactive Theorem Proving ITP 2015. An extended version of this publication is available here.
[2015-03-17] Added pairing heaps by Hauke Brinkop.
[2016-07-12] Moved splay heaps from here to Splay_Tree
[2016-07-14] Moved pairing heaps from here to the new Pairing_Heap
Robin EΓmann π§, Tobias Nipkow π, Simon Robillard π and Ujkan Sulejmani +
Robin EΓmann π§, Tobias Nipkow π, Simon Robillard π and Ujkan Sulejmani
January 16, 2020
[2015-09-23] Salomon Sickert added an interface that does not require the usage of the Boolean formula datatype. Furthermore the general Mapping type is used instead of an association list.
Javier Esparza π, Peter Lammich π, RenΓ© Neumann π§, Tobias Nipkow π, Alexander Schimpf π§ and Jan-Georg Smaus π +
Javier Esparza π, Peter Lammich π, RenΓ© Neumann π§, Tobias Nipkow π, Alexander Schimpf π§ and Jan-Georg Smaus π
May 28, 2014
An early version of this model checker is described in the CAV 2013 paper with the same title.
[2020-04-14] Incorporate Time_Monad of the AFP entry Root_Balanced_Tree.
Manuel Eberl π, Johannes HΓΆlzl π and Tobias Nipkow π +
Manuel Eberl π, Johannes HΓΆlzl π and Tobias Nipkow π
October 9, 2014
An article with the same title and authors is published in the proceedings of ESOP 2015. A detailed presentation of this work can be found in the first author's master's thesis.
A full description is found in a companion paper.
[2010-11-02] modified theories to reflect the modified definition of tameness in Hales' revised proof.
[2014-07-03] modified constants in def of tameness and Archive according to the final state of the Flyspeck proof.
Tobias Nipkow π and Lawrence C. Paulson π +
Tobias Nipkow π and Lawrence C. Paulson π
November 7, 2008
Maximilian P. L. Haslbeck π and Tobias Nipkow π +
Maximilian P. L. Haslbeck π and Tobias Nipkow π
February 17, 2016
These theories formalize the quantitative analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The material is based on the first two chapters of Online Computation and Competitive Analysis by Borodin and El-Yaniv.
For an informal description see the FSTTCS 2016 publication Verified Analysis of List Update Algorithms by Haslbeck and Nipkow.
Dmitriy Traytel π and Tobias Nipkow π +
Dmitriy Traytel π and Tobias Nipkow π
June 12, 2014
Decision procedures for regular expression equivalence have been formalized before, usually based on Brzozowski derivatives. Yet, for a straightforward embedding of MSO formulas into regular expressions an extension of regular expressions with a projection operation is required. We prove total correctness and completeness of an equivalence checker for regular expressions extended in that way. We also define a language-preserving translation of formulas into regular expressions with respect to two different semantics of MSO.
The formalization is described in this ICFP 2013 functional pearl.
Johannes HΓΆlzl π and Tobias Nipkow π +
Johannes HΓΆlzl π and Tobias Nipkow π
January 3, 2012
As application of these models we formalize probabilistic model checking of pCTL formulas, analysis of IPv4 address allocation in ZeroConf and an analysis of the anonymity of the Crowds protocol. See here for the corresponding paper.
Dongchen Jiang π§ and Tobias Nipkow π +
Dongchen Jiang π§ and Tobias Nipkow π
December 17, 2010
[2011-09-09] Added Rado's proof
Tobias Nipkow π and Simon RoΓkopf π +
Tobias Nipkow π and Simon RoΓkopf π
April 27, 2021
Wolfgang Naraschewski and Tobias Nipkow π +
Wolfgang Naraschewski and Tobias Nipkow π
March 19, 2004
Simon Wimmer π, Shuwei Hu π§ and Tobias Nipkow π +
Simon Wimmer π, Shuwei Hu π§ and Tobias Nipkow π
May 22, 2018
Klaus Aehlig π and Tobias Nipkow π +
Klaus Aehlig π and Tobias Nipkow π
February 18, 2008
Hauke Brinkop π§ and Tobias Nipkow π +
Hauke Brinkop π§ and Tobias Nipkow π
July 14, 2016
The amortized complexity of pairing heaps is analyzed in the AFP article Amortized Complexity.
Origin: This library was extracted from Amortized Complexity and extended.
Peter Lammich π and Tobias Nipkow π +
Peter Lammich π and Tobias Nipkow π
June 25, 2019
[2019-12-16] Added theory Priority_Queue_Braun2 with second version of del_min
Peter Lammich π and Tobias Nipkow π +
Peter Lammich π and Tobias Nipkow π
June 25, 2019
Julius Michaelis π and Tobias Nipkow π +
Julius Michaelis π and Tobias Nipkow π
June 21, 2017
Tobias Nipkow π and Dmitriy Traytel π +
Tobias Nipkow π and Dmitriy Traytel π
January 30, 2014
Alexander Krauss π and Tobias Nipkow π +
Alexander Krauss π and Tobias Nipkow π with contributions from Manuel Eberl π and Christian Urban π
May 12, 2010
Extended regular expressions with complement and intersection are also defined and an equivalence checker is provided.
[2011-08-26] Christian Urban added a theory about derivatives and partial derivatives of regular expressions
[2012-05-10] Tobias Nipkow added equivalence checking with partial derivatives
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.
The amortized complexity of skew heaps is analyzed in the AFP entry Amortized Complexity.
The amortized complexity of splay trees and heaps is analyzed in the AFP entry Amortized Complexity.
[2016-07-12] Moved splay heaps here from Amortized_Complexity
Andreas Lochbihler π and Tobias Nipkow π +
Andreas Lochbihler π and Tobias Nipkow π
March 30, 2015
Origin: This article was extracted from existing articles by the authors.