Reseña: Philosophy of mathematics and computer science

PorJosé A. Alonso

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.

Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude

PorJosé A. Alonso

EL 29 de Octubre se publicó un nuevo artículo de vrificación: Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude, Science of Computer Programming en la revista Science of Computer Programming.

Los autores del artículo son Kyungmin Bae (de la University de Illinois en Urbana-Champaign), Peter Csaba Olveczky (de la Universidad de Oslo), Thomas Huining Feng, Edward A. Lee y Stavros Tripakis (los tres últimos, de la Universidad de California en Berkeley).

El resumen del artículo es

This paper defines a real-time rewriting logic semantics for a significant subset of Ptolemy II discrete-event models. This is a challenging task, since such models combine a synchronous fixed-point semantics with hierarchical structure, explicit time, and a rich expression language. The code generation features of Ptolemy II have been leveraged to automatically synthesize a Real-Time Maude verification model from a Ptolemy II design model, and to integrate Real-Time Maude verification of the synthesized model into Ptolemy II. This enables a model-engineering process that combines the convenience of Ptolemy II DE modeling and simulation with formal verification in Real-Time Maude. We illustrate such formal verification of Ptolemy II models with three case studies.

Una versión previa del artículo, de libre acceso, es Verifying Hierarchical Ptolemy II discrete-event models using Real-Time Maude.

Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

PorJosé A. Alonso

Se ha publicado un nuevo artículo de formalización: Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks

Los autores del artículo son Freek Verbeek y Julien Schmaltz de la Universiad de Radboud en Nimega (en neerlandés: Nijmegen), Paises Bajos.

El artículo se publicó ayer (18 de Septiembre de 2010) en el Journal of Automated Reasoning.

Una versión preliminar del artículo puede leerse aquí y el código ACL2 correspondiente puede obtenerse aquí

El artículo es una demostración en ACL2 de una condición necesaria y suficiente para enrutamiento sin estancamiento introducida por William J. Dally y Charles L. Seitz en su artículo Deadlock Free Message Routing in Multiprocessor Interconnection Networks de 1987.
Read More “Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks”

Anuncio: Trace-based verification of imperative programs with I/O

PorJosé A. Alonso

Gregory Malecha, Greg Morrisett y Ryan Wisnesky han publicado el artículo Trace-based verification of imperative programs with I/O en el Journal of Symbolic Computation. Una versión del artículo puede leerse aquí.

El resumen del artículo es

In this paper we demonstrate how to prove the correctness of systems implemented using low-level imperative features like pointers, files, and socket I/O with respect to high level I/O protocol descriptions by using the Coq proof assistant. We present a web-based course gradebook application developed with Ynot, a Coq library for verified imperative programming. We add a dialog-based I/O system to Ynot, and we extend Ynot’s underlying Hoare logic with event traces to reason about I/O and protocol behavior. Expressive abstractions allow the modular verification of both high level specifications like privacy guarantees and low level properties like data structure pointer invariants.

Los autores son miembros del Grupo de Lenguajes de Programación de la Universidad de Harvard.

Este artículo está relacionado con el proyecto SAFE (Semantically Aware Foundation Environment) comentado en una entrada anterior.