From Tarski to Hilbert

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento aproximado en Coq sobre geometría titulado From Tarski to Hilbert.

Sus autores son Gabriel Braun y Julien Narboux (de la Universidad de Estrasburgo, Francia).

Su resumen es

In this paper, we report on the formal proof that Hilbert’s axiom system can be derived from Tarski’s system. For this purpose we mechanized the proofs of the first twelve chapters of Schwabauser, Szmielew and Tarski’s book: Metamathematische Methoden in der Geometrie. The proofs are checked formally within classical logic using the Coq proof assistant. The goal of this development is to provide clear foundations for other formalizations of geometry and implementations of decision procedures.

El trabajo se ha presentado en el ADG 2012 (Automated Deduction in Geometry 2012)

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

Generic datatypes à la carte

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en Coq titulado Generic datatypes à la carte.

Sus autores son Steven Keuchel y Tom Schrijvers (de la Universidad de Gante, Bélgica).

Su resumen es

Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory à la Carte (MTC) framework in the context of programming language meta-theory. However, MTC’s use of extensible Church-encodings is unsatisfactory.

This paper takes a better approach to the problem with datatype- generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.

El correspondiente código en Coq se encuentra aquí.

El trabajo se presentará en el WGP 2013 (9th ACM SIGPLAN Workshop on Generic Programming).

Mechanized metatheory for a λ λ-calculus with trust types

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Mechanized metatheory for a λ λ-calculus with trust types.

Sus autores son

Su resumen es

As computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a λ λ -calculus with trust types, originally formulated by Ørbæk and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.

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

La versión final del trabajo se ha publicado en el Journal of the Brazilian Computer Society.

A computer-assisted proof of correctness of a marching cubes algorithm

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado A computer-assisted proof of correctness of a marching cubes algorithm.

Sus autores son Andrey N. Chernikov y Jing Xu (de la Old Dominion University, Norfolk, EEUU).

Su resumen

The Marching Cubes algorithm is a well known and widely used approach for extracting a triangulated isosurface from a three-dimensional rectilinear grid of uniformly sampled data values. The algorithm relies on a large manually constructed table which exhaustively enumerates all possible patterns in which the isosurface can intersect a cubical cell of the grid. For each pattern the table con- tains the local connectivity of the triangles. The construction of this table is labor intensive and error prone. Indeed, the original paper allowed for topological holes in the surface. This problem was later fixed by several authors, however a formal proof of correctness to our knowledge was never presented. In our opinion the most reliable approach to constructing a formal proof for this algorithm is to write a computer program which checks that all the entries in the table satisfy some sufficient condition of correctness. In this paper we present our formal proof which follows this approach, developed with the Coq proof assistant software. The script of our proof can be executed by Coq which verifies that the proof is logically correct, in the sense that its conclusions indeed logically follow from the assumptions. Coq offers a number of helpful features that automate proof development. However, Coq cannot check that the development corresponds to the problem we wish to solve, therefore, this correspondence is elaborated upon in this paper. Our complete Coq development is available online.

El trabajo se presentará en octubre en el 22nd International Meshing Roundtable.

Reseña: “Proofs you can believe in – Proving equivalences between Prolog semantics in Coq”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Proofs you can believe in (Proving equivalences between Prolog semantics in Coq).

Sus autores son

El trabajo se presentará en septiembre en el PPDP 2013 (15th International Symposium on Principles and Practice of Declarative Programming ).

Su resumen es

Basing program analyses on formal semantics has a long and successful tradition in the logic programming paradigm. These analyses rely on results about the relative correctness of mathematically sophisticated semantics, and authors of such analyses often invest considerable effort into establishing these results. The development of interactive theorem provers such as Coq and their recent successes both in the field of program verification as well as in mathematics, poses the question whether these tools can be usefully deployed in logic programming. This paper presents formalisations in Coq of several general results about the correctness of semantics in different styles; forward and backward, top-down and bottom-up. The results chosen are paradigmatic of the kind of correctness theorems that semantic analyses rely on and are therefore well-suited to explore the possibilities afforded by the application of interactive theorem provers to this task, as well as the difficulties likely to be encountered in the endeavour. It turns out that the advantages offered by moving to a functional setting, including the possibility to apply higher-order abstract syntax, are considerable.

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