Introducción a la realizabildad

  • Mauricio Guillermo. Universidad de la República, Uruguay
  • Track de Fundamentos de Lenguajes de Programación.

Nota: El curso será dictado en Español

Resumen

La Realizabilidad consiste en definir una semántica polivalente, asociando a cada fórmula matemática un valor de verdad. Esos valores de verdad pueden ser de los más 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á énfasis 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ún 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