Reseña

Se ha publicado un nuevo artículo de automatización del razonamiento en Coq sobre metateorías de lenguajes de programación: Meta-theory à la carte.

Sus autores son Benjamin Delaware, Bruno C. d. S. Oliveira y Tom Schrijvers.

Su resumen es

Formalizing meta-theory, or proofs about programming languages, in a proof assistant has many well-known benefits. However, the considerable effort involved in mechanizing proofs has prevented it from becoming standard practice. This cost can be amortized by reusing as much of an existing formalization as possible when building a new language or extending an existing one. Unfortunately reuse of components is typically ad-hoc, with the language designer cutting and pasting existing definitions and proofs, and expending considerable effort to patch up the results.

This paper presents a more structured approach to the reuse of formalizations of programming language semantics through the composition of modular definitions and proofs. The key contribution is the development of an approach to induction for extensible Church encodings which uses a novel reinterpretation of the universal property of folds. These encodings provide the foundation for a framework, formalized in Coq, which uses type classes to automate the composition of proofs from modular components.

Several interesting language features, including binders and general recursion, illustrate the capabilities of our framework. We reuse these features to build fully mechanized definitions and proofs for a number of languages, including a version of mini-ML. Bounded induction enables proofs of properties for non-inductive semantic functions, and mediating type classes enable proof adaptation for more feature-rich languages.

El marco descrito en el artículo, así como el caso de estudio de mini-ML se encuentra en Meta-Theory à la Carte + Modular mini-ML.

Se ha publicado un nuevo artículo de razonamiento formalizado en Coq sobre cálculo numérico: Rigorous polynomial approximation using Taylor models in Coq.

Sus autores son Nicolas Brisebarre, Mioara Maria Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca,
Laurence Rideau y Laurent Théry. Todos son miembros del grupo CoqApprox.

El trabajo se ha desarrollado dentro del proyecto TaMaDi y se presentó el 5 de abril en el NFM 2012 (4th NASA Formal Methods Symposium).

El resumen del trabajo es

One of the most common and practical ways of representing a real function on machines is by using a polynomial approximation. It is then important to properly handle the error introduced by such an approximation. The purpose of this work is to offer guaranteed error bounds for a specific kind of rigorous polynomial approximation called Taylor model. We carry out this work in the Coq proof assistant, with a special focus on genericity and efficiency for our implementation. We give an abstract interface for rigorous polynomial approximations, parameterized by the type of coefficients and the implementation of polynomials, and we instantiate this interface to the case of Taylor models with interval coefficients, while providing all the machinery for computing them. We compare the performances of our implementation in Coq with those of the Sollya tool, which contains an implementation of Taylor models written in C. This is a milestone in our long-term goal of providing fully formally proved and efficient Taylor models.

Este trabajo es continuación de la tesis doctoral de Mioara Joldes titulada Rigorous polynomial approximations and applications, dirigida por Nicolas Brisebarre y Jean-Michel Muller presentada el 26 de septiembre de 2011 en la Universidad de Lyon.

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