Reseña: Light-weight containers for Isabelle: efficient, extensible, nestable

Se ha publicado un artículo de verificación formal en Isabelle/HOL titulado Light-weight containers for Isabelle: efficient, extensible, nestable.

Su autor es Andreas Lochbihler (del ETH Zürich).

El trabajo se presentará en julio en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

In Isabelle/HOL, we develop an approach to efficiently implement container types such as sets and maps in generated code. Thanks to type classes and refinement during code generation, our light-weight framework is flexible, extensible, and easy to use. To support arbitrary nesting of containers, we devise an efficient linear order on sets that can even compare complements and non-complements. Our evaluation shows that it is both efficient and usable.

Los códigos de las correspondientes teorías en Isabelle/HOL se encuentran aquí.