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.

Reseña: Numerical analysis of ordinary differential equations in Isabelle/HOL

PorJosé A. Alonso

El miércoles (15 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Isabelle/HOL titulado Numerical analysis of ordinary differential equations in Isabelle/HOL

Sus autores son Fabian Immler y Johannes Hölzl (de la Technische Universität München).

El resumen del trabajo es

Many ordinary differential equations (ODEs) do not have a closed solution, therefore approximating them is an important problem in numerical analysis. This work formalizes a method to approximate solutions of ODEs in Isabelle/HOL.

We formalize initial value problems (IVPs) of ODEs and prove the existence of a unique solution, i.e. the Picard-Lindelöf theorem. We introduce generic one-step methods for numerical approximation of the solution and provide an analysis regarding the local and global error of one-step methods.

We give an executable specification of the Euler method as an instance of one-step methods. With user-supplied proofs for bounds of the differential equation we can prove an explicit bound for the global error. We use arbitrary-precision floating-point numbers and also handle rounding errors when we truncate the numbers for efficiency reasons.

El código de la formalización en Isabelle/HOL se encuentra aquí.

Reseña: Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un trabajo de razonamiento formalizado en Isabelle/HOL, titulada Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL.

Su autor es Jose Divasón Mallagaray, dirigido por Jesús María Aransay Azofra (de la Univ. de la Rioja).

La presentación del trabajo tuvo lugar el 25 de Octubre de 2011 en la Universidad de la Rioja.

El objetivo del trabajo es la formalización en Isabelle/HOL de conceptos y teoremas sobre álgebra lineal siguiendo la 16 primeras secciones del libro de Halmos Finite-dimensional vector spaces.

El resumen del trabajo es

In this work we deal with finite-dimensional vector spaces over a generic field \mathbb{K}. First we will state properties of vector spaces independently of their dimension. Then, we will introduce the conditions to obtain finite-dimensional vector spaces. The notions of linear dependence and independence, as well as linear combinations, and hence the notion of basis will be presented. Some results about the dimension of the different basis of a vector space will be necessary, as well as on the isomorphism among vector spaces. Once we have introduced the notion of basis, and with the additional condition of it being finite, we will introduce the notion of finite-dimensional vector space. Next step is to introduce vector subspaces. We will pay attention to vector susbpaces generated by a given set of vectors and prove some of their properties. The notion of linear maps will be also required to define isomorphisms of vector spaces. Finally, we will prove that a vector space (over a field \mathbb{K}) of (finite) dimension n is isomorphic to \mathbb{K}^n.

The previous results will be presented following the book by Halmos on vector spaces [1]. Its formalization will be carried out in Isabelle/HOL.

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

Una extensión del trabajo es Formalizing an abstract algebra textbook in Isabelle/HOL presentado el 14 de junio de 2012 en el EACA 2012 (EACA 2012
XIII Encuentro de Álgebra Computacional y Aplicaciones).

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

Reseña: Towards provably robust watermarking

PorJosé A. Alonso

El martes (14 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado Towards provably robust watermarking.

Sus autores son David Baelde, Pierre Courtieu, David Gross-Amblard y
Christine Paulin-Mohring.

El resumen del trabajo es

Watermarking techniques are used to help identifying copies of publicly released information. They consist in applying a slight and secret modification to the data before its release, in a way that should be robust, ie., remain recognizable even in (reasonably) modified copies of the data. In this paper, we present new results about the robustness of watermarking schemes against arbitrary attackers, and the formalization of those results in Coq. We used the ALEA library, which formalizes probability theory and models probabilistic programs using a simple monadic translation. This work illustrates the strengths and particularities of the induced style of reasoning about probabilistic programs. Our technique for proving robustness is adapted from methods commonly used for cryptographic protocols, and we discuss its relevance to the field of watermarking.

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

El trabajo es parte del proyecto SCALP (Security of Cryptographic ALgorithms with Probabilities).

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