Reseña: Amortized complexity verified

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Amortized complexity verified.

Su autor es Tobias Nipkow (de la Technische Universität München).

Su resumen es

*A framework for the analysis of the amortized complexity of (functional) data structures is formalized in Isabelle/HOL and applied to two non-trivial examples: skew heaps and splay trees. In the same spirit we show that the move-to-front algorithm for the list update problem is 2-competitive. *

El trabajo se presentó en el Isabelle Workshop 2014.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.