Verified Analysis of List Update Algorithms

Maximilian P.L. Haslbeck and Tobias Nipkow

This paper presents a machine-verified 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 analysis is verified with help of the theorem prover Isabelle.



  author ={Maximilian P. L. Haslbeck and Tobias Nipkow},
  title ={{Verified Analysis of List Update Algorithms}},
  booktitle ={36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages ={49:1--49:15},
  series ={Leibniz International Proceedings in Informatics (LIPIcs)},
  year ={2016},
  volume ={65},
  editor ={Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
  publisher ={Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  URL ={},
  doi ={}
Online article

Isabelle theories in the Archive of Formal Proofs