Menu Close

Etiqueta: Coq

RA2018: Razonamiento automático con Coq

En la clase de hoy del curso de Razonamiento automático se ha explicado cómo se puede usar Coq como alternativa a Isabelle/HOL que hemos utilizado anteriormente en el curso.

Los temas, con las correspondientes teorías de Coq, que se han explicado

Reseña: Proving tree algorithms for succinct data structures

Se ha publicado un artículo de razonamiento formalizado en Coq sobre algorítmica titulado Proving tree algorithms for succinct data structures.

Sus autores son

Su resumen es

Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different succinct tree algorithms. One is the Level-Order Unary Degree Sequence (aka LOUDS), which encodes the structure of a tree in breadth first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary red-black trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient Insert and Delete. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.

El trabajo se ha presentado el 30 de agosto en el JSSST 2018 (The 35th Meeting of the Japan Society for Software Science and Technology).

El código de las correspondientes teorías se encuentra GitHub.

Reseña: Formal verification of a geometry algorithm (A quest for abstract views and symmetry in Coq proofs)

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs.

Su autor es Yves Bertot (del grupo MARELLE del INRIA, Sophia Antipolis).

Su resumen es

This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex notions are those of boundary and separating edges. When performing proofs about this algorithm, questions of symmetry appear and this exposition attempts to give an account of how these symmetries can be handled. All this work relies on formal developments made with Coq and the mathematical components library.

El trabajo se presentará el 16 de octubre en el ICTAC 2018 (15th International Colloquium on Theoretical Aspects of Computing).

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

Reseña: “Concrete semantics” with Coq and CoqHammer

Se ha publicado un artículo de razonamiento formalizado en Coq titulado “Concrete semantics” with Coq and CoqHammer.

Sus autores son

Su resumen es

The “Concrete Semantics” book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant. In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness, and the readability of the proof scripts originating from a Coq re-formalization of two chapters from the book.

El trabajo se ha presentado el 15 de agosto en el CICM 2018 (11th Conference on Intelligent Computer Mathematics).

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

Hammer for Coq (automation for dependent type theory)

Se ha publicado un artículo sobre automatización del razonamiento titulado Hammer for Coq (automation for dependent type theory).

Sus autores son Łukasz Czajka (de la Universidad de Varsovia) y Cezary Kaliszyk (del Computational Logic group la Universidad de Innsbruck).

Su resumen es

Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, the construction of hammers for such foundations has been hindered so far by the lack of translation and reconstruction components. In this paper, we present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is “sufficiently” sound and complete to be of practical use for automated theorem provers. We also introduce a proof reconstruction mechanism based on an eauto-type algorithm combined with limited rewriting, congruence closure and some forward reasoning. The algorithm is able to re-prove in the Coq logic most of the theorems established by the ATPs. Together with machine-learning based selection of relevant premises this constitutes a full hammer system. The performance of the whole procedure is evaluated in a bootstrapping scenario emulating the development of the Coq standard library. For each theorem in the library only the previous theorems and proofs can be used. We show that 40.8% of the theorems can be proved in a push-button mode in about 40 s of real time on a 8-CPU system.

El trabajo se ha publicado en el Journal of Automated Reasoning.

El código de CoqHammer se encuentra en GitHub.

Reseña: Comparison of two theorem provers: Isabelle/HOL and Coq

Se ha publicado un artículo de demostración asistida por ordenador titulado Comparison of two theorem provers: Isabelle/HOL and Coq.

Sus autores son

Su resumen es

The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although, according to Gödel’s incompleteness theorems, it is not possible to construct a single formal system which will describe all phenomena in the world, being complete and consistent at the same time, it gave rise to rather practical areas of logic, such as the theory of automated theorem proving. This is a set of techniques used to verify mathematical statements mechanically using logical reasoning. Moreover, it can be used to solve complex engineering problems as well, for instance, to prove the security properties of a software system or an algorithm. This paper compares two widespread tools for automated theorem proving, Isabelle/HOL and Coq, with respect to expressiveness, limitations and usability. For this reason, it firstly gives a brief introduction to the bases of formal systems and automated deduction theory, their main problems and challenges, and then provides detailed comparison of most notable features of the selected theorem provers with support of illustrative proof examples.

Programación funcional y métodos elementales de demostración en Coq

En este tema se introduce mediante ejemplos la programación funcional en Coq y la demostración de las propiedades de las funciones definidas usando los métodos elementales de programación en Coq.

Su contenido es

  1. Datos y funciones
    1. Tipos enumerados
    2. Booleanos
    3. Tipos de las funciones
    4. Tipos compuestos
    5. Módulos
    6. Números naturales
  2. Métodos elementales de demostración
    1. Demostraciones por simplificación
    2. Demostraciones por reescritura
    3. Demostraciones por análisis de casos

La teoría correspondiente es