Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre algorítmica titulado Balancing lists: a proof pearl.

Sus autores son Guyslain Naves (de la Aix-Marseille University) y Arnaud Spiwack (de Inria Paris-Rocquencourt).

Su resumen es

Starting with an algorithm to turn lists into full trees which uses non-obvious invariants and partial functions, we progressively encode the invariants in the types of the data, removing most of the burden of a correctness proof.

The invariants are encoded using non-uniform inductive types which parallel numerical representations in a style advertised by Okasaki, and a small amount of dependent types.

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

Se ha publicado un artículo de razonamiento formalizado en Coq sobre coindución titulado Moessner’s theorem: an exercise in coinductive reasoning in Coq.

Sus autores son

• Robbert Krebbers (de la Univ. de Nimeja, Paises Bajos),
• Louis Parlant (de la Escuela Normal Superior de Lyon, Francia) y
• Alexandra Silva (de la Univ. de Nimeja, Paises Bajos)

Su resumen es

Moessner’s Theorem describes a construction of the sequence of powers (1ⁿ, 2ⁿ, 3ⁿ,…), by repeatedly dropping and summing elements from the sequence of positive natural numbers. The theorem was presented by Moessner in 1951 without a proof and later proved and generalized in several directions. More recently, a coinductive proof of the original theorem was given by Niqui and Rutten. We present a formalization of their proof in the Coq proof assistant. This formalization serves as a non-trivial illustration of the use of coinduction in Coq. In the process of formalizing the original proof we discovered that Long and Salié’s generalization of Moessner’s Theorem could also be proved using (almost) the same bisimulation.

El trabajo se presentó en el seminario del COIN (Coalgebra in the Netherlands) . Las transparencias de la presentación se encuentran aquí.

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

Se ha publicado un artículo de razonamiento formalizado en Coq sobre la semántica del lenguaje C titulado Aliasing restrictions of C11 formalized in Coq.

Su autor es Robbert Krebbers (de la Radboud University Nijmegen, Holanda).

Su resumen es

The C11 standard of the C programming language describes dynamic typing restrictions on memory operations to make more effective optimizations based on alias analysis possible. These restrictions are subtle due to the low-level nature of C, and have not been treated in a formal semantics before. We present an executable formal memory model for C that incorporates these restrictions, and at the same time describes required low-level operations.

Our memory model and essential properties of it have been fully formalized using the Coq proof assistant.

Este trabajo forma parte del proyecto CH₂O cuyo objetivo es la formalización del estándard C11 del lenguaje de programación C.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

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

Se ha publicado un artículo de razonamiento formalizado en Coq sobre refinamientos de datos titulado Refinements for free!.

Sus autores son

• Cyril Cohen (de la Univ. de Gotemburgo, Suecia),
• Maxime Dénès (de la Univ. de Pensilvania, EE.UU.) y
• Anders Mörtberg (de la Univ. de Gotemburgo, Suecia).

Su resumen es

Formal verification of algorithms often requires a choice between definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopting a high-level view when proving correctness and then refining stepwise down to an efficient low-level implementation. Some refinement steps are interesting, in the sense that they improve the algorithms involved, while others only express a switch from data representations geared towards proofs to more efficient ones geared towards computations. We relieve the user of these tedious refinements by introducing a framework where correctness is established in a proof-oriented context and automatically transported to computation-oriented data structures. Our design is general enough to encompass a variety of mathematical objects, such as rational numbers, polynomials and matrices over refinable structures. Moreover, the rich formalism of the Coq proof assistant enables us to develop this within Coq, without having to maintain an external tool.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).