Reseña: Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)

Se ha publicado un artículo sobre formalización en Isabelle/Isar titulado Reading an algebra textbook.

Su autor es Clemens Ballarin (de la Technische Universität München) y lo presentó en el CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

We report on a formalisation experiment where excerpts from an algebra textbook are compared to their translation into formal texts of the Isabelle/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising.

Reseña: “The formalization of syntax-based mathematical algorithms using quotation and evaluation”

Se ha publicado un artículo sobre formalización de algoritmos titulado The formalization of syntax-based mathematical algorithms using quotation and evaluation.

Su autor es William M. Farmer (de la McMaster University, Canadá) y lo presentará en las CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen

Algorithms like those for differentiating functional expressions manipulate the syntactic structure of mathematical expressions in a mathematically meaningful way. A formalization of such an algorithm should include a specification of its computational behavior, a specification of its mathematical meaning, and a mechanism for applying the algorithm to actual expressions. Achieving these goals requires the ability to integrate reasoning about the syntax of the expressions with reasoning about what the expressions mean. A syntax framework is a mathematical structure that is an abstract model for a syntax reasoning system. It contains a mapping of expressions to syntactic values that represent the syntactic structures of the expressions; a language for reasoning about syntactic values; a quotation mechanism to refer to the syntactic value of an expression; and an evaluation mechanism to refer to the value of the expression represented by a syntactic value. We present and compare two approaches, based on instances of a syntax framework, to formalize a syntax-based mathematical algorithm in a formal theory T. In the first approach the syntactic values for the expressions manipulated by the algorithm are members of an inductive type in T, but quotation and evaluation are functions defined in the metatheory of T. In the second approach every expression in T is represented by a syntactic value, and quotation and evaluation are operators in T itself.

Reseña: Proof pearl – A mechanized proof of GHC’s mergesort

Se publicado un artículo de verificación en Iabelle/HOL titulado Proof pearl – A mechanized proof of GHC’s mergesort.

Su autor es Christian Sternagel (de la Univ. de la Univ. de Insbruck).

Su resumen es

We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art poof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.

La librería estándard de GHC (The Glasgow Haskell Compiler) tiene un algoritmo de ordenación, que es una variante de la ordenación por mezcla. El objetivo del trabajo es la verificación de dicho algortimo en Isabelle/HOL, demostrando su corrección y estabilidad.

La principal característica de este trabajo es la verificación de programas eficientes. El método empleado tiene tres pasos:

  1. formalizar variantes del algoritmo que faciliten la demostración y probar todas las propiedades deseadas;
  2. formalizar variantes eficientes del algoritmo y probar su equivalencia y
  3. usar la generación de código y obtener un programa eficiente del que se tiene garantía que satisface todas las propiedades que se probaron en la formalización inicial.

La formalización es pequeña (menos de 400 líneas de código) y la mayoría de las demostraciones son automáticas. Este éxito se basa en dos principios: la generalización de los conceptos y la definición de esquemas de inducción.

El código en Isabelle/HOL de la teoría correspondiente al trabajo se encuentra en The Archive of Formal Proofs.

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

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: Interactive and automated proofs for graph transformations

Se ha publicado un trabajo de razonamiento formalizado en Isabelle/HOL titulado Interactive and automated proofs for graph transformations.

Su autor es Martin Strecker (de la Univ. Paul Sabatier, Toulouse, Francia).

Su resumen es

This article explores methods to provide computer support for reasoning about graph transformations. We first define a general framework for representing graphs, graph morphisms and single graph rewriting steps. This setup allows for interactively reasoning about graph transformations. In order to achieve a higher degree of automation, we identify fragments of the graph description language in which we can reduce reasoning about global graph properties to reasoning about local properties, involving only a bounded number of nodes, which can be decided by Boolean satisfiability solving or even by deterministic computation of low complexity.

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