Commit dd92ff84 authored by gerwin.klein@nicta.com.au's avatar gerwin.klein@nicta.com.au
Browse files

last merge from afp-2014

......@@ -892,7 +892,10 @@ abstract =
A framework for the analysis of the amortized complexity of (functional)
data structures is formalized in Isabelle/HOL and applied to a number of
standard examples and to the folowing non-trivial ones: skew heaps,
splay trees, splay heaps and pairing heaps.
splay trees, splay heaps and pairing heaps. This work is described
in a <a href="http://www.in.tum.de/~nipkow/pubs/itp15.html">paper</a>
published in the proceedings of the conference on Interactive
Theorem Proving ITP 2015.
<p>
In the same spirit we show that the move-to-front algorithm for the list
update problem is 2-competitive and that this is optimal for deterministic
......
@string{IPL="Information Processing Letters"}
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
@string{Springer="Springer-Verlag"}
@book{Cormen-Leiserson-Rivest,
author="Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest",
......@@ -23,6 +22,11 @@ title="Introduction to Algorithms",publisher="MIT Press",year=1990}
title="The derivation of a tighter bound for top-down skew heaps",
journal=IPL,volume=37,pages={265-271},year=1991}
@inproceedings{Nipkow-ITP15,author={Tobias Nipkow},
title={Amortized Complexity Verified},
booktitle={Interactive Theorem Proving (ITP 2015)},
editor={Ch. Urban},publisher="Springer",series=LNCS,year=2015}
@book{Okasaki,author="Chris Okasaki",title="Purely Functional Data Structures",
publisher="Cambridge University Press",year=1998}
......
......@@ -23,7 +23,8 @@
A framework for the analysis of the amortized complexity of (functional)
data structures is formalized in Isabelle/HOL and applied to a number of
standard examples and to the following non-trivial ones: skew heaps,
splay trees, splay heaps and pairing heaps.
splay trees, splay heaps and pairing heaps. This work is described
in an ITP 2015 paper~\cite{Nipkow-ITP15}.
In the same spirit we show that the move-to-front algorithm for the list
update problem is 2-competitive and that this is optimal for deterministic
......
......@@ -47,7 +47,10 @@
A framework for the analysis of the amortized complexity of (functional)
data structures is formalized in Isabelle/HOL and applied to a number of
standard examples and to the folowing non-trivial ones: skew heaps,
splay trees, splay heaps and pairing heaps.
splay trees, splay heaps and pairing heaps. This work is described
in a <a href="http://www.in.tum.de/~nipkow/pubs/itp15.html">paper</a>
published in the proceedings of the conference on Interactive
Theorem Proving ITP 2015.
<p>
In the same spirit we show that the move-to-front algorithm for the list
update problem is 2-competitive and that this is optimal for deterministic
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment