I1M2014: El TAD de los polinomios en Haskell

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos estudiado el tipo abstracto de los polinomios y su implementación en Haskell.

Comenzamos la clase analizando las posibles representaciones de los polinomios y, como consecuencia, establecer la signatura y las propiedades del TAD de los polinomios.

A continuación, estudiamos tres prosibles representaciones del TAD de los polinomios mediante tipos algebraicos, mediantes listas dispersas y mediante listas densas y sus implementaciones en Haskell

Finalmente, hemos estudiado las operaciones con los polinomios usando el TAD de los polinomios.

Las transparencias usadas en la clase son las del tema 21

El código del TAD de polinomios mediante tipo algebraico es
Read More “I1M2014: El TAD de los polinomios en Haskell”

Reseña: Verifying fast and sparse SSA-based optimizations in Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre
compiladores titulado Verifying fast and sparse SSA-based optimizations in Coq .

Sus autores son Delphine Demange, David Pichardie y Léo Stefanesco (del grupo Celtique en el INRIA Rennes, Francia).

Su resumen es

The Static Single Assignment (SSA) form is a predominant technology in modern compilers, enabling powerful and fast program optimizations. Despite its great success in the implementation of pro- duction compilers, it is only very recently that this technique has been introduced in verified compilers. As of today, few evidence exist on that, in this context, it also allows faster and simpler optimizations. This work builds on the CompCertSSA verified compiler (an SSA branch of the verified CompCert C compiler). We implement and verify two prevail- ing SSA optimizations: Sparse Conditional Constant Propagation and Global Value Numbering. For both transformations, we mechanically prove their soundness in the Coq proof assistant. Both optimization proofs are embedded in a single sparse optimization framework, factoring out many of the dominance-based reasoning steps required in proofs of SSA-based optimizations. Our experimental evaluations indicate both a better precision, and a significant compilation time speedup.

El trabajo se presentará en CC 2015 (24th International Conference on Compiler Construction).

El código de las correspondientes teorías en Coq se encuentra aquí.

Reseña: Formal proofs for nonlinear optimization

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Formal proofs for nonlinear optimization.

Sus autores son

Su resumen es

We present a formally verified global optimization framework. Given a semialgebraic or transcendental function f and a compact semialgebraic domain K, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of f over K.

This method allows to bound in a modular way some of the constituents of f by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations.

Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent.

The application range for such a tool is widespread; for instance Hales’ proof of Kepler’s conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature.

El trabajo se ha publicado en el Journal of Formalized Reasoning.

El código de las correspondientes teorías en Coq se encuentra aquí.

Reseña: Mutual exclusion by four shared bits with not more than quadratic complexity

Se ha publicado un artículo de razonamiento formalizado en PVS sobre concurrencia titulado Mutual exclusion by four shared bits with not more than quadratic complexity.

Su autor es Wim H. Hesselink (de la Universidad de Groninga, Países Bajos).

Su resumen es

For years, the mutual exclusion algorithm of Lycklama and Hadzilacos (1991) was the optimal mutual exclusion algorithm with the first-come-first-served property, with a minimal number of (non-atomic) communication variables (5 bits per thread). Recently, Aravind published an improvement of it, which uses 4 bits per threads and has simplified waiting conditions. This algorithm is extended here with fault tolerance, and it is verified by assertional methods, using the proof assistant PVS. Progress is proved by means of UNITY logic. The paper proposes a new measure of concurrent time complexity, and proves that the concurrent complexity for throughput of the present algorithm is not more than quadratic in the number of threads.

El código de las correspondientes teorías en PVS se encuentra aquí.