Reseña: A constructive theory of regular languages in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado A constructive theory of regular languages in Coq.

Sus autores son Christian Doczkal, Jan-Oliver Kaiser y Gert Smolka (de la Univ. de Sarre (en alemán: Saarland), Alemania).

Su resumen es

We present a formal constructive theory of regular languages consisting of about 1400 lines of Coq/Ssreflect. As representations we consider regular expressions, deterministic and nondeterministic automata, and Myhill and Nerode partitions. We construct computable functions translating between these representations and show that equivalence of representations is decidable. We also establish the usual closure properties, give a minimization algorithm for DFAs, and prove that minimal DFAs are unique up to state renaming. Our development profits much from Ssreflect’s support for finite types and graphs.

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

Reseña: Formalization of real analysis: A survey of proof assistants and libraries

PorJosé A. Alonso

Se ha publicado un artículo sobre razonamiento formalizado titudado Formalization of real analysis: A survey of proof assistants and libraries.

Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond.

Su resumen es

In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability, and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the proof automations these systems provide for real analysis.

Reseña: Homotopy limits in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Homotopy limits in Coq.

Sus autores son Jeremy Avigad (de la Carnegie Mellon University), Krzysztof Kapulkin (de la Univ. de Pittsburgh) y Peter LeFanu Lumsdaine.

Su resumen es

Working in Homotopy Type Theory, we provide a systematic study of basic homotopy limits and related constructions. The entire development has been formally verified in the Coq interactive proof assistant.

Las teorías en Coq correspondientes al artículo se encuentra aquí.

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í.