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í.

Reseña: “Certified, efficient and sharp univariate Taylor models in Coq”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Certified, efficient and sharp univariate Taylor models in Coq.

Sus autores son

Su resumen es

We present a formalisation, within the COQ proof assistant, of univariate Taylor models. This formalisation being executable, we get a generic library whose correctness has been formally proved and with which one can effectively compute rigorous and sharp approximations of univariate functions composed of usual functions such as 1/x, sqrt(x), exp(x), sin(x) among others. In this paper, we present the key parts of the formalisation and we evaluate the quality of our certified library on a set of examples.

Reseña: “Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de conjuntos titulado Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁.

Sus autores son Michael Norrish (del (Canberra Research Lab., NICTA) y Brian Huffman (de Galois, Inc.).

El trabajo se ha presentado esta semana en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

We describe a comprehensive HOL mechanisation of the theory of ordinal numbers, focusing on the basic arithmetic operations. Mechanised results include the existence of fixpoints such as ε₀ , the existence of normalforms, and the validation of algorithms used in the ACL2 theorem-proving system.

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

Reseña: Program verification based on Kleene algebra in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Program verification based on Kleene algebra in Isabelle/HOL.

Sus autores son Alasdair Armstrong, Georg Struth y Tjark Weber (los dos primeros de la Universidad de Sheffield y el tercero de la de Uppsala).

El trabajo se ha presentado esta semana en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Reseña: Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)

PorJosé A. Alonso

Se ha publicado un artículo sobre formalización en Isabelle/Isar titulado Reading an algebra textbook.

Su autor es Clemens Ballarin (de la Technische Universität München) y lo presentó en el CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

We report on a formalisation experiment where excerpts from an algebra textbook are compared to their translation into formal texts of the Isabelle/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising.