Balancing lists: a proof pearl

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre algorítmica titulado Balancing lists: a proof pearl.

Sus autores son Guyslain Naves (de la Aix-Marseille University) y Arnaud Spiwack (de Inria Paris-Rocquencourt).

Su resumen es

Starting with an algorithm to turn lists into full trees which uses non-obvious invariants and partial functions, we progressively encode the invariants in the types of the data, removing most of the burden of a correctness proof.

The invariants are encoded using non-uniform inductive types which parallel numerical representations in a style advertised by Okasaki, and a small amount of dependent types.

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

RA2013: Deducción natural en lógica de primer orden con Isabelle/HOL

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha presentado la deducción natural en lógica de primer orden con Isabelle/HOL. La presentación se basa en los ejemplos de tema 8 del curso de Lógica informática), que a su vez se basa en el capítulo 2 del libro de de Huth y Ryan Logic in Computer Science (Modelling and reasoning about systems).

La página al lado de cada ejemplo indica la página de las transparencias donde se encuentra la demostración.

Para cada ejemplo se presentan distintas demostraciones. La primera intenta reflejar la demostración de las transparencias, las siguientes van eliminando detalles de la prueba hasta la última que es automática.

A los largos de los ejemplos se van comentando los elementos del lenguaje conforme van entrando en el juego.

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2013: Deducción natural en lógica de primer orden con Isabelle/HOL”

Verifying document confidentiality of a conference management system

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Verifying document confidentiality of a conference management system.

Sus autores son Sudeep Kanav, Peter Lammich y Andrei Popescu (de la Universidad Técnica de Munich).

Su resumen es

We present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality properties. The various theoretical and practical challenges posed by this development led to some novel security model and verification method that we hope is reusable for other multi-user document management systems.

El juego de Oslo en Haskell

PorJosé A. Alonso

En el número especial de la revista Mundo científico sobre El universo de los números se presenta el juego de Oslo. En dicho juego
se trata de obtener cualquier número natural no nulo, por medio de aplicaciones sucesivas de una de las reglas siguientes:

  1. poner un cero al final del número,
  2. poner un cuatro al final del número y
  3. dividir por 2 si el número es par.

Por ejemplo, el 3 y el 5 se pueden obtener como sigue

En la siguiente relación de ejercicios (elaborada para I1M) veremos qué números se pueden alcanzar, cómo y en cuántos pasos. Además, se presentan distintas soluciones comparando sus eficiencias.
Read More “El juego de Oslo en Haskell”