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: “Formalizing cut elimination of coalgebraic logics in Coq”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre metalógica titulado Formalizing cut elimination of coalgebraic logics in Coq.

Su autor es Hendrik Tews (de la Dresden University of Technology) y se presentará en el Tableaux 2013 (Automated Reasoning with Analytic Tableaux and Related Methods).

Su resumen es

In their work on coalgebraic logics, Pattinson and Schröder prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics. The present paper reports on a formalization of Pattinson’s and Schröder’s work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.

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

Reseña: “Formalizing bounded increase”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre terminación titulado Formalizing bounded increase.

Su autor es René Thiemann (de la Univ. de Innsbruck, Austria) y lo presentará en la ITP 2013 (4th International Conference on Interactive Theorem Proving).

Su resumen es

Bounded increase is a termination technique where it is tried to find an argument x of a recursive function that is increased repeatedly until it reaches a bound b, which might be ensured by a condition x < b. Since the predicates like < may be arbitrary user-defined recursive functions, an induction calculus is utilized to prove conditional constraints. In this paper, we present a full formalization of bounded increase in the theorem prover Isabelle/HOL. It fills one large gap in the pen-and-paper proof, and it includes generalized inference rules for the induction calculus as well as variants of the Babylonian algorithm to compute square roots. These algorithms were required to write executable functions which can certify untrusted termination proofs from termination tools that make use of bounded increase. And indeed, the resulting certifier was already useful: it detected an implementation error that remained undetected since 2007.