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: Proving concurrent noninterference

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 Isabelle/HOL titulado Proving concurrent noninterference.

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (del grupo de demostración automática (Theorem Proving Group) de la Universidad de Munich).

Su resumen es

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of noninterference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

Este trabajo forma parte del proyecto Security Type Systems and Deduction

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

Reseña: Formalizing Frankl’s conjecture: FC-families

PorJosé A. Alonso

En las CICM 2012 (Conferences on Intelligent Computer Mathematics) se ha presentado un trabajo de razonamiento formalizado en Isabelle/HOL titulado Formalizing Frankl’s conjecture: FC-families.

Sus autores son Filip Marić, Miodrag Živković y Bojan Vučković (del grupo ARGO (Automated Reasoning GrOup) de la Universidad de Belgrado).

Su resumen es

The Frankl’s conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. FC-families are families for which it is proved that every union-closed family containing them satisfies the Frankl’s condition (e.g., in every union-closed family that contains a one- element set a, the element a is contained in at least half of the sets, so families of the form a are the simplest FC-families). FC-families play an important role in attacking the Frankl’s conjecture, since they enable significant search space pruning. We present a formalization of the computer assisted approach for proving that a family is an FC-family. Proof-by-computation paradigm is used and the proof assistant Isabelle/HOL is used both to check mathematical content, and to perform (verified) combinatorial searches on which the proofs rely. FC-families known in the literature are confirmed, and a new FC-family is discovered.

El código con la formalización en Isabelle/HOL se encuentra aquí.

PeH: Piensa en Haskell (Ejercicios de programación funcional con Haskell)

PorJosé A. Alonso

He publicado la primera versión de libro Piensa en Haskell (Ejercicios de programación funcional con Haskell).

Este libros es una introducción a la programación funcional con Haskell a través de una colección de ejercicios resueltos de los cursos de Informática (del
Grado en Matemáticas) y Programación declarativa (de la Ingeniería en Informática).

Los temas correspondientes a los ejercicios del libro se encuentra en Temas de programación funcional.

El libro consta de tres partes. En la primera parte se presentan los elementos básicos de la programación funcional. En la segunda, se estudian la implementación en Haskell de tipos abstractos de datos y sus aplicaciones así como cuestiones algorítmicas. En la tercera, se presentan casos de estudios. También se han incluido dos apéndices: uno con un resumen de las funciones de Haskell utilizadas y otro con el método de Pólya para la resolución de problemas.
Read More “PeH: Piensa en Haskell (Ejercicios de programación funcional con Haskell)”