I1M2015: Comienzo del curso
El curso Informática (de 1º de Grado en Matemáticas) comenzarán el miércoles 23 de septiembre.
Las clases son los miércoles y viernes de 9:00 a 11:00.
La página con los materiales del curso se encuentra aquí.
Reseña: Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda
Se ha publicado un artículo de razonamiento formalizado en Agda titulado Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda.
Sus autores son Ernesto Copello, Álvaro Tasistro y Bruno Bianchi (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).
Su resumen es
We present a full certification of merge sort in the language Agda. It features: termination warrant without explicit proof, no proof cost to ensure that the output is sorted, and a succinct proof that the output is a permutation of the input.
El trabajo se ha presentado en The Brazilian Symposium on Programming Languages (SBLP).
El código de las correspondientes teorías en Agda se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.
LI2015: Comienzo del curso
El curso Lógica informática (de 2º de Grado en Ingeniería Informática) comienza el martes 22 de septiembre.
Las clases son los martes y jueves de 10:30 a 12:30 en el aula A0.11 de la ETSII.
La página con los materiales del curso se encuentra aquí.
Reseña: Formalization of Shannon’s theorems
Se ha publicado un artículo de razonamiento formalizado en Coq sobre teoría de la información titulado Formalization of Shannon’s theorems.
Sus autores son
- Reynald Affeldt (del AIST (National Institute of Advanced Industrial Science and Technology) en Tsukuba, Japón),
- Manabu Hagiwara (de la Chiba University en Chiba, Japón) y
- Jonas Sénizergues (de la Ecole Normale Supérieure de Cachan, France).
Su resumen es
The most fundamental results of information theory are Shannon’s theorems. These theorems express the bounds for (1) reliable data compression and (2) data transmission over a noisy channel. Their proofs are non-trivial but are rarely detailed, even in the introductory literature. This lack of formal foundations is all the more unfortunate that crucial results in computer security rely solely on information theory: this is the so-called “unconditional security”. In this article, 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 of the channel coding theorem, that introduces the capacity as the bound for reliable communication over a noisy channel.
El artículo, publicado en el JAR, es una extensión del trabajo Formalization of Shannon’s Theorems in SSReflect-Coq presentado en el ITP 2012.
El código de las correspondientes teorías en Coq se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.
Reseña: Decreasing diagrams for Church-Rosser modulo
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre reescritura titulado Decreasing diagrams for Church-Rosser modulo.
Su autor es Bertram Felgenhauer (del Computational Logic Research Group en la Universidad de Innsbruck, Austria).
Su resumen es
This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides important specializations, in particular van Oostrom’s conversion version (TCS 2008) of decreasing diagrams.
We follow the development described in 1: Conversions are mapped to Greek strings, and we prove that whenever a local peak (or cliff) is replaced by a joining sequence from a locally decreasing diagram, then the corresponding Greek strings become smaller in a specially crafted well-founded order on Greek strings. Once there are no more local peaks or cliffs are left, the result is a valley that establishes the Church-Rosser modulo property.
As special cases we provide non-commutation versions and the conversion version of decreasing diagrams by van Oostrom 3. We also formalize extended decreasingness 2.
El trabajo se ha publicado en The Archive of Formal Proofs.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.
Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.