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

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.

Applications of the Gauss-Jordan algorithm, done right

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado Applications of the Gauss-Jordan algorithm, done right.

Sus autores son Jesús María Aransay y José Divasón (de la Univ. de la Rioja).

Su resumen es

Computer Algebra systems are widely spread because of some of their remarkable features such as their ease of use and performance. Nonetheless, this focus on performance sometimes leads to unwanted consequences: algorithms and computations are implemented and carried out in a way which is sometimes not transparent to the users, and that can lead to unexpected failures.

In this paper we present a formalisation in a proof assistant system of a naive version of the Gauss-Jordan algorithm, with explicit proofs of some of its applications, and additionally a process to obtain versions of this algorithm in two different functional languages (SML and Haskell) by means of code generation techniques from the verified algorithm. The obtained programs are then applied to test cases, which, despite the simplicity of the original algorithm, have shown remarkable features in comparison to some Computer Algebra systems, such as Mathematica (where some of these computations are even incorrect), or Sage (in comparison to which the generated programs show a compelling performance).

The aim of the paper is to show that, with the current technology in Theorem Proving, formalising Linear Algebra procedures is a challenging but rewarding task, which provides programs that can be compared in some aspects to state of the art procedures in Computer Algebra systems, and whose correctness is formally proved.

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

Formal kinematic analysis of the two-link planar manipulator

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL Light sobre cinemática titulado Formal kinematic analysis of the two-link planar manipulator.

Sus autores son Binyameen Farooq, Osman Hasan, Sohail Iqbal (de la Universidad de Islamabad, Pakistán).

Su resumen es

Kinematic analysis is used for trajectory planning of robotic manipulators and is an integral step of their design. The main idea behind kinematic analysis is to study the motion of the robot based on the geometrical relationship of the robotic links and their joints. Given the continuous nature of kinematic analysis, traditional computer-based verification methods, such as simulation, numerical methods or model checking, fail to provide reliable results. This fact makes robotic designs error prone, which may lead to disastrous consequences given the safety-critical nature of robotic applications. Leveraging upon the high expressiveness of higher-order logic, we propose to use higher-order-logic theorem proving for conducting formal kinematic analysis. As a first step towards this direction, we utilize the geometry theory of HOL-Light to develop formal reasoning support for the kinematic analysis of a two-link planar manipulator, which forms the basis for many mechanical structures in robotics. To illustrate the usefulness of our foundational formalization, we present the formal kinematic analysis of a biped walking robot.

El trabajo se ha presentado en el ICFEM 2013 (15th International Conference on Formal Engineering Methods). Las trasparencias de la presentación se encuentran aquí.

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

Structural induction principles for functional programmers

PorJosé A. Alonso

Se ha publicado un artículo sobre la automatización del razonamiento titulado Structural induction principles for functional programmers.

Su autor es James Caldwell (de la Universidad de Wyoming).

Su resumen es

User defined recursive types are a fundamental feature of modern functional programming languages like Haskell, Clean, and the ML family of languages. Properties of programs defined by recursion on the structure of recursive types are generally proved by structural induction on the type. It is well known in the theorem proving community how to generate structural induction principles from data type declarations. These methods deserve to be better know in the functional programming community. Existing functional programming textbooks gloss over this material. And yet, if functional programmers do not know how to write down the structural induction principle for a new type – how are they supposed to reason about it? In this paper we describe an algorithm to generate structural induction principles from data type declarations. We also discuss how these methods are taught in the functional programming course at the University of Wyoming. A Haskell implementation of the algorithm is included in an appendix.

El trabajo se ha publicado en los Proceedings Second Workshop on Trends in Functional Programming In Education.