Reseña: Coinductive pearl: Modular first-order logic completeness

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Coinductive pearl: Modular first-order logic completeness.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

Codatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.

El código de las teorías Isabelle correspodientes se encuentra aquí.

Reseña: Experience report: Teaching Haskell to the masses

PorJosé A. Alonso

Se ha publicado un artículo sobre la ensñanza de Haskell titulado Experience report: Teaching Haskell to the masses.

Sus autores son Jasmin Christian Blanchette, Tobias Nipkow, Lars Noschinski y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

We report on our experience teaching a Haskell-based functional programming course to over 600 students. The syllabus was organized around selected material from various sources. Throughout the term, we emphasized correctness through QuickCheck tests and proofs by induction. The submission architecture was coupled with automatic testing, giving students the possibility to correct mistakes before the deadline. To motivate the students, we complemented the weekly assignments with an informal competition.

Reseña: Square root and division elimination in PVS

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en PVS titulado Square root and division elimination in PVS.

Su autor es Pierre Neron (del INRIA en Paris – Rocquencourt).

El trabajo se presentará en julio en el ITP 2013 (4th Conference on Interactive Theorem Proving).

Su resumen es

In this paper we present a new strategy for PVS that implements a square root and division elimination in order to use automatic arithmetic strategies that were not able to deal with these operations in a first place. This strategy relies on a PVS formalization of the square root and division elimination and deep embedding of PVS expressions inside PVS. Therefore using computational reflection and symbolic computation we are able to automatically transform expressions into division and square root free ones before using these decisions procedures.

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

Reseña: One logic to use them all

PorJosé A. Alonso

Una de las principales barreras en el avance de la automatización del razonamiento consiste en la comunicación entre distintos sistemas de razonamiento. Una forma de superarla es la planteada en el artículo One logic to use them all.

Su autor es Jean-Christophe Filliâtre (de la Universidad de París-Sur).

El trabajo se presentará en el CADE-24 (24th International Conference on Automated Deduction).

Su resumen es

Deductive program verification is making fast progress these days. One of the reasons is a tremendous improvement of theorem provers in the last two decades. This includes various kinds of automated theorem provers, such as ATP systems and SMT solvers, and interactive proof assistants. Yet most tools for program verification are built around a single theorem prover. Instead, we defend the idea that a collaborative use of several provers is a key to easier and faster verification. This paper introduces a logic that is designed to target a wide set of theorem provers. It is an extension of first-order logic with polymorphism, algebraic data types, recursive definitions, and inductive predicates. It is implemented in the tool Why3, and has been successfully used in the verification of many non-trivial programs.

Reseña: Automating inductive proofs using theory exploration

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento automático sobre programas funcionales en Haskell titulado Automating inductive proofs using theory exploration.

Sus autores son Koen Claessens, Moa Johansson, Dan Rosén y Nicholas Smallbone (de la Universidad de Chalmers).

El trabajo se presentará en el CADE-24 (24th International Conference on Automated Deduction).

Su resumen es

HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.

El código de HipSpec se encuentra en aquí. Los experimentos con HipSpec se encuentran aquí.