Reseña: Operational refinement for compiler correctness

PorJosé A. Alonso

Este mes (septiembre de 2012) se va a presentar en la Universidad de Princeton una tesis doctoral de verificación formal en Coq titulada Operational refinement for compiler correctness.

Su autor es Robert W. Dockins, dirigido por Andrew W. Appel.

Su resumen es

Compilers are an essential part of the software development process. Programmers all over the world rely on compilers every day to correctly translate their intentions, expressed as high-level source code, into executable low-level machine code. But what does it mean for a compiler to be correct?

This question is surprisingly difficult to answer. Despite the fact that various groups have made concerted efforts to prove the correctness of compilers since at least the early 1980’s, no clear consensus has arisen about what it means for a compiler to be correct. As a result, it seems that no two compiler verification efforts have stated their correctness theorems in the same way.

In this dissertation, I will advance a new approach to compiler correctness based on refinements of the operational semantics of programs. The cornerstones of this approach are behavioral refinement, which allows programs to improve by going wrong less often, and choice refinement, which allows compilers to reduce the amount of internal nondeterminism present in a program. I take particular care to explain why these notions of refinement are the correct formal interpretations of the informal ideas above.

In addition, I will show how these notions of refinement can be realistically applied to compiler verification efforts. First, I will present a toy language, WHILE-C, and show how choice and behavioral refinement can be used to verify the correctness of several interesting program transformations. The WHILE-C language and the transformations themselves are simple enough to be presented here in full detail. I will also show how the ideas of behavioral and choice refinement may be applied to the CompCert formally verified compiler [Ler09a], a realistic compiler for a significant subset of C

El código Coq correspondiente a la tesis se encuentra aquí.

Esta tesis se enmarca en el proyecto Verified Software Toolchain.

Reseña: Formalization and verification of number theoretic algorithms using the Mizar proof checker

PorJosé A. Alonso

En el FCS’12 (The 2012 International Conference on Foundations of Computer Science) se presentó un trabajo de razonamiento formalizado en Mizar titulado Formalization and verification of number theoretic algorithms using the Mizar proof checker.

Sus autores son Hiroyuki Okazaki, Yoshiki Aoki y Yasunari Shidama (de la Shinshu University).

Su resumen es

In this paper, we introduce formalization of well-known number theoretic algorithms on the Mizar proof checking system. We formalized the Euclidean algorithm, the extended Euclidean algorithm and the algorithm computing the solution of the Chinese reminder theorem based on the source code of NZMATH which is a Python based number theory oriented calculation system. We prove the accuracy of our formalization using the Mizar proof checking system as a formal verification tool.

Reseña: Deriving a fast inverse of the generalized Cantor N-tupling bijection

PorJosé A. Alonso

La semana que viene (6 de septiembre) se presentará en el ICLP’12 (28th International Conference on Logic Programming) un trabajo sobre resolución lógica de problemas combinatorios titulado Deriving a fast inverse of the generalized Cantor N-tupling bijection.

Su autor es Paul Tarau (de la University of North Texas, Denton, Texas, USA).

Su resumen es

We attack an interesting open problem (an efficient algorithm to invert the generalized Cantor N-tupling bijection) and solve it through a sequence of equivalence preserving transformations of logic programs, that take advantage of unique strengths of this programming paradigm. An extension to set and multiset tuple encodings, as well as a simple application to a “fair-search” mechanism illustrate practical uses of our algorithms.

The code in the paper (a literate Prolog program, tested with SWI-Prolog and Lean Prolog) is available at http://logic.cse.unt.edu/tarau/research/2012/pcantor.pl.

Reseña: Logic + control: An example of program construction

PorJosé A. Alonso

Se ha publicado un trabajo sobre metodología de la programación en Prolog titulado Logic + control: An example of program construction.

Su autor es Wlodzimierz Drabent (de la Univ. de Linköping, Suecia).

El trabajo se presentará el 6 de Septiembre en el ICLP’12 (28th International Conference on Logic Programming).

Su resumen es

We present a Prolog program (the SAT solver of Howe and King) as a logic program with added control. The control consists of a selection rule (delays of Prolog) and pruning the search space. We construct the logic program together with proofs of its correctness and completeness, with respect to a formal specification. This is augmented by a proof of termination under any selection rule. Correctness and termination are inherited by the Prolog program, the change of selection rule preserves completeness. We prove that completeness is also preserved by one case of pruning; for the other an informal justification is presented.

For proving correctness we use a method, which should be well known but is often neglected. A contribution of this paper is a method for proving completeness. In particular we introduce a notion of semi-completeness, for which a local sufficient condition exists.

We compare the proof methods with declarative diagnosis (algorithmic debugging). We introduce a method of proving that a certain kind of pruning preserves completeness. We argue that the proof methods correspond to natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.

Reseña: Coherent and strongly discrete rings in type theory

PorJosé A. Alonso

Se ha publicado un nuevo trabajo de formalización de las matemáticas en Coq titulado Coherent and strongly discrete rings in type theory.

Sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).

El trabajo se presentará en el CPP 2012 (The Second International Conference on Certified Programs and Proofs) que comenzará el 13 de diciembre.

Su resumen es

We present a formalization of coherent and strongly discrete rings in type theory. This is a fundamental structure in constructive algebra that represents rings in which it is possible to solve linear systems of equations. These structures have been instantiated with Bézout domains (for instance \mathbb{Z} and k[x]) and Prüfer domains (generalization of Dedekind domains) so that we get certified algorithms solving systems of equations that are applicable on these general structures. This work can be seen as basis for developing a formalized library of linear algebra over rings.

El código Coq de la formalización se encuentra aquí.

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.