Reseña: Compositional verification of a communication protocol for a remotely operated aircraft

La semana pasada se publicó un nuevo artículo de verificación formal con PVS: Compositional verification of a communication protocol for a remotely operated aircraft.

Los autores del artículo son Alwyn E. Goodloe and César A. Muñoz.

El resumen del artículo es

This paper presents the formal specification and verification of a communication protocol between a ground station and a remotely operated aircraft. The protocol can be seen as the vertical composition of protocol layers, where each layer performs input and output message processing, and the horizontal composition of different processes concurrently inhabiting the same layer, where each process should satisfy a distinct delivery requirement. A compositional technique is used to formally prove that the protocol satisfies these requirements. Although the protocol itself is not novel, the methodology employed in its verification extends existing techniques by automating the tedious and usually cumbersome part of the proof, thereby making the iterative design process of protocols feasible.

En la Red se publicó una versión preliminar del artículo.

Reseña: Coq, a proof assistant based on higher-order intuitionistic type theory

La semana pasada Jean-Pierre Jouannaud hizo una presentación sobre razonamiento automático en el Instituto de estudios avanzados de la Universidad de Tsinghua: Coq, a proof assistant based on higher-order intuitionistic type theory.

En la presentación se incluyen comentarios sobre objetivos y logros del razonamiento formalizado, los fundamentos teóricos de los demostradores, la correspondencia de Curry-Horward, el cálculo de construcciones de Coq y su adecuación.

Reseña: Philosophy of mathematics and computer science

Kazimierz Trzęsicki (del Departamento de Lógica, Informática y Filosofía de la Ciencia de la Universidad de Białystok, Polonia) ha publicado el artículo Philosophy of mathematics and computer science.

El resumen del artículo es

It is well known fact that the foundation of modern computer science were laid by logicians. Logic is at the heart of computing. The development of contemporary logic and the problems of the foundations of mathematics were in close mutual interaction. We may ask why the concepts and theories developed out of philosophical motives before computers were even invented, prove so useful in the practice of computing. Three main programmes together with the constructivist approach are discussed and the impact on computer science is considered.

En el artículo comenta las aportaciones a la ciencia de la computación de las tres escuelas lógicas de los fundamentos de la matemática:

  • del logicismo (de Frege, Russell y Withehead) resalta el sintaxis de la lógica como primer lenguaje de programación, los tipos, el lamda cálculo, LISP, la programación funcional y la lógica combinatoria como lenguaje de programación.
  • del formalismo (de Hilbert) destaca la máquina de Turing (como medio para resolver los problemas de decibilidad), la teoría de la computación, la demostración automática y el razonamiento formalizado.
  • del intuicionismo (de Brouwer) y del constructivismo (de Markov y Bishop) destaca la visión de “fórmulas-como-tipos”, la extracción de programas a partir de las pruebas, la teoría costructiva de tipos de Martin-Löf, los sistema de demostración asistida (Automath, NuPRL, LEGO, Agda, Twelf y Coq) y las teorías desarrolladas con dichos sistemas.

Reseña: Formalization of propositional linear temporal logic in the Mizar system

Una línea de trabajo dentro del campo del razonamiento formalizado consiste en la formalización de la metalógica de distintos sistemas lógicos. En esta línea se inscribe el artículo Formalization of propositional linear temporal logic in the Mizar system.

Su autor es Mariusz Giero (University of Bialystok).

Su resumen es

The paper describes formalization of some issues of propositional linear temporal logic (PLTL). We discuss encountered problems and applied solutions. The formalization was carried out in the Mizar system. In comparison with other systems, Mizar is famous for its large repository of computer checked mathematical knowledge and also for its user-friendly knowledge representation and proof language.

Reseña: Implementation of Bourbaki’s Elements of Mathematics in Coq. Part Two: Ordered Sets, Cardinals, Integers

En una entrada anterior comentamos el proyecto de formalización del libro Elements of Mathematics: Theory of Sets de N. Bourbaki en Coq.

En dicha entrada comentamos el primer paso del proyecto consistente en la formalización de la teoría de conjuntos correspondiente al capítulo II del libro de Bourbaki (páginas 65-130).

La formalización del capítulo III (páginas 131-256) constituye el contenido del segundo paso. Dicha formalización ha sido publicada por José Grimm en el artículo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. Su resumen es el siguiente

We believe that it is possible to put the whole work of Bourbaki into a computer. One of the objectives of the Gaia project concerns homological algebra (theory as well as algorithms); in a first step we want to implement all nine chapters of the book Algebra. But this requires a theory of sets (with axiom of choice, etc.) more powerful than what is provided by Ensembles; we have chosen the work of Carlos Simpson as basis. This reports lists and comments all definitions and theorems of the Chapter Ordered Sets, Cardinals, Integers”.

Version 3 is based on the Coq ssreflect library. It implements some properties on ordinal numbers. The code (including some exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia.