Reseña: Computing persistent homology within Coq/SSReflect

PorJosé A. Alonso

Se ha publicado un nuevo trabajo de razonamiento formalizado en Coq titulado Computing persistent homology within Coq/SSReflect.

Sus autores son Jónathan Heras, Thierry Coquand, Anders Mörtbeg y Vincent Siles.

Su resumen es

Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this paper, we report on the formal development of certified programs to compute persistent Betti numbers, an instrumental tool of persistent homology, using the Coq proof assistant together with the SSReflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.

Reseña: Improving real analysis in Coq: a user-friendly approach to integrals and derivatives

PorJosé A. Alonso

En la CPP 2012 (The Second International Conference on Certified Programs and Proofs), que comenzará el 13 de diciembre, se presentará un trabajo de verificación formal en Coq titulado Improving real analysis in Coq: a user-friendly approach to integrals and derivatives.

Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond (del grupo ProVal (Proof of Programs) en el INRIA Saclay – Île-de-France).

Su resumen es

Verification of numerical analysis programs requires dealing with derivatives and integrals. High confidence in this process can be achieved using a formal proof checker, such as Coq. Its standard library provides an axiomatization of real numbers and various lemmas about real analysis, which may be used for this purpose. Unfortunately, its definitions of derivative and integral are unpractical as they are partial functions that demand a proof term. This proof term makes the handling of mathematical formulas cumbersome and does not conform to traditional analysis. Other proof assistants usually do not suffer from this issue; for instance, they may rely on Hilbert’s epsilon to get total operators. In this paper, we propose a way to define total operators for derivative and integral without having to extend Coq’s standard axiomatization of real numbers. We proved the compatibility of our definitions with the standard library’s in order to leverage existing results. We also greatly improved automation for real analysis proofs that use Coq standard definitions. We exercised our approach on lemmas involving iterated partial derivatives and differentiation under the integral sign, that were missing from the formal proof of a numerical program solving the wave equation.

Este trabajo forma parte del proyecto Coquelicot.

El código con las teorías correspondiente se encuentra aquí.

Reseña: Operational refinement for compiler correctness

PorJosé A. Alonso

Este mes (septiembre de 2012) se va a presentar en la Universidad de Princeton una tesis doctoral de verificación formal en Coq titulada Operational refinement for compiler correctness.

Su autor es Robert W. Dockins, dirigido por Andrew W. Appel.

Su resumen es

Compilers are an essential part of the software development process. Programmers all over the world rely on compilers every day to correctly translate their intentions, expressed as high-level source code, into executable low-level machine code. But what does it mean for a compiler to be correct?

This question is surprisingly difficult to answer. Despite the fact that various groups have made concerted efforts to prove the correctness of compilers since at least the early 1980’s, no clear consensus has arisen about what it means for a compiler to be correct. As a result, it seems that no two compiler verification efforts have stated their correctness theorems in the same way.

In this dissertation, I will advance a new approach to compiler correctness based on refinements of the operational semantics of programs. The cornerstones of this approach are behavioral refinement, which allows programs to improve by going wrong less often, and choice refinement, which allows compilers to reduce the amount of internal nondeterminism present in a program. I take particular care to explain why these notions of refinement are the correct formal interpretations of the informal ideas above.

In addition, I will show how these notions of refinement can be realistically applied to compiler verification efforts. First, I will present a toy language, WHILE-C, and show how choice and behavioral refinement can be used to verify the correctness of several interesting program transformations. The WHILE-C language and the transformations themselves are simple enough to be presented here in full detail. I will also show how the ideas of behavioral and choice refinement may be applied to the CompCert formally verified compiler [Ler09a], a realistic compiler for a significant subset of C

El código Coq correspondiente a la tesis se encuentra aquí.

Esta tesis se enmarca en el proyecto Verified Software Toolchain.

Reseña: Coherent and strongly discrete rings in type theory

PorJosé A. Alonso

Se ha publicado un nuevo trabajo de formalización de las matemáticas en Coq titulado Coherent and strongly discrete rings in type theory.

Sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).

El trabajo se presentará en el CPP 2012 (The Second International Conference on Certified Programs and Proofs) que comenzará el 13 de diciembre.

Su resumen es

We present a formalization of coherent and strongly discrete rings in type theory. This is a fundamental structure in constructive algebra that represents rings in which it is possible to solve linear systems of equations. These structures have been instantiated with Bézout domains (for instance \mathbb{Z} and k[x]) and Prüfer domains (generalization of Dedekind domains) so that we get certified algorithms solving systems of equations that are applicable on these general structures. This work can be seen as basis for developing a formalized library of linear algebra over rings.

El código Coq de la formalización se encuentra aquí.

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.

Reseña: A refinement-based approach to computational algebra in Coq

PorJosé A. Alonso

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado A refinement-based approach to computational algebra in Coq.

Sus autores son Maxime Dénès (del INRIA Sophia Antipolis, Francia) y Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).

El resumen del trabajo es

We describe a step-by-step approach to the implementation and formal verification of efficient algebraic algorithms. Formal specifications are expressed on rich data types which are suitable for deriving essential theoretical properties. These specifications are then refined to concrete implementations on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank computation, Winograd’s fast matrix product, Karatsuba’s polynomial multiplication, and the gcd of multivariate polynomials.

El código de la formalización en Coq se encuentra aquí.

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.