Reseña: Construction of real algebraic numbers in Coq

PorJosé A. Alonso

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado Construction of real algebraic numbers in Coq.

Su autor es Cyril Cohen (de la École Polytechnique (Palaiseau, Francia)).

El resumen del trabajo es

This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.

El código de la formalización en Coq se encuentra en realalg.tgz.

Reseña: Abstract interpretation of annotated commands

PorJosé A. Alonso

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle titulado Abstract interpretation of annotated commands.

Su autor es Tobias Nipkow (del Theorem Proving Group de la Technische Universität München).

El resumen del trabajo es

This paper formalises a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalisation, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.

Las correspondientes teorías de Isabelle se encuentran aquí.

Reseña: Formalization of Shannon’s theorems in SSReflect-Coq

PorJosé A. Alonso

Se ha publicado un nuevo artículo de razonamiento formalizado en Coq, titulado Formalization of Shannon’s theorems in SSReflect-Coq.

Sus autores son Reynald Affeldt y Manabu Hagiwara (del National Institute of Advanced Industrial Science and Technology en Tsukuba, Japón).

El trabajo se presentó ayer en el ITP 2012 (Interactive Theorem Proving).

El resumen del trabajo es

The most fundamental results of information theory are Shannon’s theorems. These theorems express the bounds for reliable data compression and transmission over a noisy channel. Their proofs are non-trivial but rarely detailed, even in the introductory literature. This lack of formal foundations makes it all the more unfortunate that crucial results in computer security rely solely on information theory (the so-called “unconditional security”). In this paper, we report on the formalization of a library for information theory in the SSReflect extension of the Coq proof-assistant. In particular, we produce the first formal proofs of the source coding theorem (that introduces the entropy as the bound for lossless compression), and the direct part of the more difficult channel coding theorem (that introduces the capacity as the bound for reliable communication over a noisy channel).

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

Reseña: Algorithms in games evolving in time: Winning strategies based on testing

PorJosé A. Alonso

Se ha publicado un nuevo artículo de razonamiento formalizado en Isabelle/HOL sobre la teoría de juegos, titulado Algorithms in games evolving in time: Winning strategies based on testing. Sus autores son Evgeny Dantsin, Jan-Georg Smaus y Sergei Soloviev y se presentará el 12 de agosto en el Isabelle Users Workshop 2012.

Su resumen es

We model two-player imperfect-information games evolving in time, where one player makes and tests “hypotheses” about the opponent’s strategies. We consider algorithms needed for the first player to compute a winning strategy. The main assumptions about the scenario are the following: (1) the hypotheses form a “covering”, i.e., each strategy of the second player satisfies at least one hypothesis; (2) the hypotheses can be enumerated and tested; (3) for each hypothesis, the first player has a strategy that “defeats” all of the opponent’s strategies satisfying this hypothesis.

We have modelled a significant part of the theory presented here in Isabelle/HOL.

Reseña: Formalizing adequacy: A case study for higher-order abstract syntax

PorJosé A. Alonso

Se ha publicado un nuevo trabajo de razonamiento formalizado en Isabelle: Formalizing adequacy: A case study for higher-order abstract syntax.

Sus autores son James Cheney, Michael Norrish y René Vestergaard.

Su resumen es

Adequacy is an important criterion for judging whether a formalization is suitable for reasoning about the actual object of study. The issue is particularly subtle in the expansive case of approaches to languages with name-binding. In prior work, adequacy has been formalized only with respect to specific representation techniques. In this article, we give a general formal definition based on model-theoretic isomorphisms or interpretations. We investigate and formalize an adequate interpretation of untyped lambda-calculus within a higher-order metalanguage in Isabelle/HOL using the Nominal Datatype Package. Formalization elucidates some subtle issues that have been neglected in informal arguments concerning adequacy.

La formalización en Isabelle se encuentra aquí.