Abstract
A partir del isomorfismo de Curry–Howard y de las teorías de tipos desarrolladas en las últimas décadas se acuñó la idea de ver a los programas como demostraciones de propiedades. Es decir, si tenemos una demostración P de un teorema T, podemos convertir a P en un programa cuyo tipo es T. Esta teoría ha dado lugar a un desarrollo revolucionario en las áreas de diseño de lenguajes de programación y sistemas de verificación de programas. Sin embargo, en esta charla, les quiero mostrar una visión alternativa y, en algún sentido, previa: programas como fórmulas. Es decir, que la misma fórmula matemática o lógica que escribamos sea un programa; o sea, que no sea necesario demostrar una propiedad para tener un programa, sino que su especificación es el programa. En este sentido les voy a mostrar el sistema {log} (setlog) que es un lenguaje de programación pero también es un demostrador automático de teoremas. En {log} las fórmulas son programas, o los programas son fórmulas. Y podemos usar el mismo sistema y el mismo lenguaje para demostrar propiedades de las fórmulas o programas. Más aun, en {log} las fórmulas son sobre la teoría de conjuntos finitos lo que permite escribir especificaciones de grandes clases de programas.
Short bio
Maximiliano Cristiá es profesor de Ingeniería de Software en la Universidad Nacional de Rosario desde 1998 e investigador del Centro Internacional Franco-Argentino de Ciencias de la Información y Sistemas (CIFASIS) desde su fundación. Realizó su maestría en computación en el InCo-PEDECIBA y su doctorado en la Universidad de Marsella.