I1M2012: El TAD de los polinomios en Haskell (2)

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos continuado el estudio del tipo abstracto de los polinomios y su implementación en Haskell que comenzamos en la clase anterior. Concretamente, hemos estudiado la implementaciones en Haskell del TAD de los polinomios mediante listas densas y las operaciones con los polinomios usando el TAD.

Las transparencias usadas en la clase son las páginas 24-55 del tema 21
Read More “I1M2012: El TAD de los polinomios en Haskell (2)”

Reseña: Data refinement in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo sobre automatización del razonamiento en Isabelle/HOL titulado Data refinement in Isabelle/HOL.

Sus autores son Florian Haftmann, Alexander Krauss, Ondřej Kunčar y Tobias Nipkow (de la Universidad Técnica de Munich).

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

Su resumen es

The paper shows how the code generator of Isabelle/HOL supports data refinement, i.e., providing efficient code for operations on abstract types, e.g., sets or numbers. This allows all tools that employ code generation, e.g., Quickcheck or proof by evaluation, to compute with these abstract types. At the core is an extension of the code generator to deal with data type invariants. In order to automate the process of setting up specific data refinements, two packages for transferring definitions and theorems between types are exploited.