Introducción a la realizabildad

  • Mauricio Guillermo. Montevideo, Uruguay
  • Track de Fundamentos de Lenguajes de Programación.

Nota: El curso será dictado en Inglés

Resumen

La Realizabilidad consiste en definir una sem´antica polivalente, asociando a cada fórmula matem´atica un valor de verdad. Esos valores de verdad pueden ser de los m´as diversos tipos, por ejemplo: enteros, elementos de un álgebra de Heyting, conjuntos de programas escritos en alguna variante de λ-cálculo o subconjuntos de un álgebra combinatoria. A diferencia de la teoría de la desmostración, cuyo énfasis está en la sintaxis, la realizabilidad interpreta a las fórmulas de un punto de vista algorítmico.
En este curso desarrollamos un panorama de temas desde los or´ıgenes de la Realizabilidad de Kleene hasta la Realizabilidad Clásica de Krivine y la Realizabilidad Concurrente de Beffara. Se pondrá ´enfasis en tópicos de teoría de modelos, de especificación de programas y de la presentación algebraica de la Realizabilidad. Para desarrollar los aspectos algebraicos se incursionará también
en los modelos categóricos de la Realizabilidad basados en Topos.

Cronograma

Día 1 Constructivismo, intuicionismo, aritmética de Heyting. Realizabilidad de Kleene.
Día 2 Realizabilidad de Kreisel. Modelos categóricos de la realizabilidad: el topos efectivo de Hayland.
Día 3 Realizabilidad de Krivine. El problema de la especificación. Modelos de la Teoría de Conjuntos en Realizabilidad Clásica.
Día 4 El modelo categórico de Streicher para la Realizabilidad de Krivine. Programa de algebrización.
Día 5 Programación concurrente. Realizabilidad Concurrente de Beffara.

Prerrequisitos

Haber hecho alg´un curso elemental de lógica y/o de λ-cálculo. Si bien el curso es autocontenido, el haber trabajado previamente con algún lenguaje formal y algún cálculo sobre ese lenguaje ayuda a la comprensión del tema.

Inscribirse
Ver todos los cursos