Reseña: Programming and reasonning with PowerLists in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre programas paralelos titulado Programming and reasonning with PowerLists in Coq.

Sus autores son

Su resumen es

For parallel programs correctness by construction is an essential feature since debugging is almost impossible. To build correct programs by constructions is not a simple task, and usually the methodologies used for this purpose are rather theoretical based on a pen-and-paper style. A better approach could be based on tools and theories that allow a user to develop an efficient parallel application by implementing easily simple programs satisfying conditions, ideally automatically, proved. PowerLists theory and the variants represent a good theoretical base for an approach like this, and Coq proof assistant is a tool that could be used for automatic proofs. The goal of this paper is to model the PowerList theory in Coq, and to use this modelling to program and reason on parallel programs in Coq. This represents the first step in building a framework that ease the development of correct and verifiable parallel programs.

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

Reseña: Formalized algebraic numbers: construction and first-order theory

PorJosé A. Alonso

Se ha publicado una tesis de razonamiento formalizado en Coq sobre los números algebraicos titulada Formalized algebraic numbers: construction and first-order theory.

Su autor es Cyril Cohen dirigido por Assia Mahboubi y Benjamin Werner (de la Escuela Politécnica de París)

Su resumen es

This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in proof assistants, Coq in our case: the intuitionistic construction of real algebraic numbers together with the proof they form a real closed field, and the programming and certification of quantifier elimination procedures for the theories of algebraically closed fields and real closed fields. In order to reach those results, we brought multiple contributions to the toolboxes and formalization and proof methodologies in Coq. More particularly, we provide in Coq/SSReflect a framework to work with quotient types. We provide a complete library about ordered and normed number algebraic structures. We wrote a short implementation of Cauchy reals together with tactics to deal easily with reasoning using assertions of the form “let n be a big enough number”, commonly used in mathematical paper proofs. We also developed a short library of real polynomial analysis. A big part of our contributions is useful for the formalization of the proof of Odd Order Theorem and they also aim at helping to prove and certify more efficient quantifier elimination procedures on reals.

La correspondientes teorías en Coq se encuentran en aquí.

Reseña: Formal reasoning about finite-state discrete-time Markov chains in HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre procesos de Markov titulado Formal reasoning about finite-state discrete-time Markov chains in HOL.

Sus autores son Liya Liu, Osman Hasan y Sofiène Tahar (de la Univ. de Concordia, Canadá).

Su resumen es

Markov chains are extensively used in modeling different aspects of engineering and scientific systems, such as performance of algorithms and reliability of systems. Different techniques have been developed for analyzing Markovian models, for example, Markov Chain Monte Carlo based simulation, Markov Analyzer, and more recently probabilistic model-checking. However, these techniques either do not guarantee accurate analysis or are not scalable. Higher-order-logic theorem proving is a formal method that has the ability to overcome the above mentioned limitations. However, it is not mature enough to handle all sorts of Markovian models. In this paper, we propose a formalization of Discrete-Time Markov Chain (DTMC) that facilitates formal reasoning about time-homogeneous finite-state discrete-time Markov chain. In particular, we provide a formal verification on some of its important properties, such as joint probabilities, Chapman-Kolmogorov equation, reversibility property, using higher-order logic. To demonstrate the usefulness of our work, we analyze two applications: a simplified binary communication channel and the Automatic Mail Quality Measurement protocol.

La revista en donde que ha publicado el artículo es el Journal of Computer Science and Technology.

Reseña: The Picard algorithm for ordinary differential equations in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre ecuaciones diferenciales titulado The Picard algorithm for ordinary differential equations in Coq.

Sus autores son Evgeny Makarov and Bas Spitters (de la Universidad de Nimega, Países Bajos).

Su resumen es

Ordinary Differential Equations (ODEs) are ubiquitous in physical applications of mathematics. The Picard-Lindelöf theorem is the first fundamental theorem in the theory of ODEs. It allows one to solve differential equations numerically. We provide a constructive development of the Picard-Lindelöf theorem which includes a program together with sufficient conditions for its correctness. The proof/program is written in the Coq proof assistant and uses the implementation of efficient real numbers from the CoRN library and the MathClasses library. Our proof makes heavy use of operators and functionals, functions on spaces of functions. This is faithful to the usual mathematical description, but a novel level of abstraction for certified exact real computation.

Las teorías desarrolladas se encuentran aquí.

Reseña: A string of pearls: Proofs of Fermat’s little theorem

PorJosé A. Alonso

En la CPP12 (The Second International Conference on Certified Programs and Proofs), que comienza el 13 de diciembre, se presentará un trabajo de razonamiento formalizado en HOL4 titulado A string of pearls: Proofs of Fermat’s little theorem.

Sus autores son Hing-Lun Chan (de la Australian National University) y Michael Norrish (del Canberra Research Lab., NICTA).

Su resumen es

We discuss mechanised proofs of Fermat’s Little Theorem in a variety of styles, focusing in particular on an elegant combinatorial “necklace” proof that has not been mechanised previously. What is elegant in prose turns out to be long-winded mechanically, and so we examine the effect of explicitly appealing to group theory. This has pleasant consequences both for the necklace proof, and also for the direct number-theoretic approach.

El código conteniendo las demostraciones en HOL4 se encuentra aquí.