El problema de las sucesiones llenas en Haskell

PorJosé A. Alonso

En las Olimpiadas de Matemáticas del 2002 se propuso el siguiente problema

Sea n un entero positivo. Una sucesión de n enteros positivos (no necesariamente distintos) se llama “llena” si verifica la siguiente condición: para cada entero positivo k ≥ 2, si el número k aparece en la sucesión, entonces también lo hace el número k-1 y, además, la primera ocurrencia de k-1 es anterior a la última ocurrencia de k. Para cada n, ¿cuántas sucesiones llenas existen?

En la siguiente relación de ejercicios, elaborada para la asignatura de Informática (de 1º del Grado en Matemáticas), se estudia con Haskell el problema.
Read More “El problema de las sucesiones llenas en Haskell”

From Tarski to Hilbert

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento aproximado en Coq sobre geometría titulado From Tarski to Hilbert.

Sus autores son Gabriel Braun y Julien Narboux (de la Universidad de Estrasburgo, Francia).

Su resumen es

In this paper, we report on the formal proof that Hilbert’s axiom system can be derived from Tarski’s system. For this purpose we mechanized the proofs of the first twelve chapters of Schwabauser, Szmielew and Tarski’s book: Metamathematische Methoden in der Geometrie. The proofs are checked formally within classical logic using the Coq proof assistant. The goal of this development is to provide clear foundations for other formalizations of geometry and implementations of decision procedures.

El trabajo se ha presentado en el ADG 2012 (Automated Deduction in Geometry 2012)

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

Computer theorem proving and HoTT

PorJosé A. Alonso

Se ha publicado un artículo sobre la demostración asistida por ordenador y los fundamentos de la matemática titulado Computer theorem proving and HoTT.

Sus autores son Joe Leslie-Hurd (de Intel Corporation) y G. McC. Haworth (de la Universidad de Reading).

Su resumen es

Theorem-proving is a one-player game. The history of computer programs being the players goes back to 1956 and the ‘LT’ Logic Theory Machine of Newell, Shaw and Simon. In game-playing terms, the ‘initial position’ is the core set of axioms chosen for the particular logic and the ‘moves’ are the rules of inference. Now, the Univalent Foundations Program at IAS Princeton and the resulting ‘HoTT’ book on Homotopy Type Theory have demonstrated the success of a new kind of experimental mathematics using computer theorem proving.

Formal verification of language-based concurrent noninterference

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Formal verification of language-based concurrent noninterference.

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (de la Universidad Técnica de Munich, Alemania).

Su resumen es

We perform a formal analysis of compositionality techniques for proving possibilistic noninterference for a while language with parallel composition. We develop a uniform framework where we express a wide range of non-interference variants from the literature and compare them w.r.t. their contracts: the strength of the security properties they ensure weighed against the harshness of the syntactic conditions they enforce. This results in a simple implementable algorithm for proving that a program has a specific noninterference property, using only compositionality, which captures uniformly several security type-system results from the literature and suggests a further improved type system. All formalism and theorems have been mechanically verified in Isabelle/HOL.

El trabajo se ha publicado en el Journal of Formalized Reasoning.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.