• 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 demostració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.

Bibliografía
[1] Emmanuel Beffara. Logique, Réalisabilité et Concurrence. Thèse de Mathématiques, spécialité Informatique. Université Paris Diderot – Paris 7, 2005. Francais. . (tesis de doctorado).
[2] Walter Ferrer Santos, Jonas Frey, Mauricio Guillermo, Octavio Malherbe, Alexandre Miquel. Ordered Combinatory Algebras and Realizability. Mathematical Structures in Computer Science, Camb. Univ. Press, 1–31 (2015).
[3] Walter Ferrer Santos, Mauricio Guillermo, Octavio Malherbe. Realizability in ordered combinatory algebras with adjunction. Mathematical Structures in Computer Science, Volume 29, Issue 3, March 2019, pp. 430 – 464.
[4] Walter Ferrer Santos, Octavio Malherbe. The category of implicative algebras and realizability. Mathematical Structures in Computer Science, Volume 29, Issue 10, November 2019, pp. 1575 – 1606.
[5] Mauricio Guillermo, Alexandre Miquel. Specifying Peirce’s law in classical realizability. Mathematical Structures in Computer Science, Volume 26, Issue 7, October 2016, pp. 1269 – 1303.
[6] Mauricio Guillermo, Etienne Miquey. ́ Classical realizability and arithmetical formulæ. Mathematical Structures in Computer Science , Volume 27 , Issue 6 , September 2017 , pp. 1068 – 1107.
[7] From Fregue to G ̈odel:A Source Book in Mathematical Logic, 1879-1931. Ed. by J.V.Heijenoort. Cambridge, Mass. Harvard University Press (2002).
[8] Jean-Louis Krivine. Realizability algebras II: new models of ZF + DC. Logical Methods in Computer Science, February 27, 2012, Volume 8, Issue 1.
[9] Jaap van Oosten. Realizability: an Introduction to its Categorical Side. vol 152 of Studies in Logic. North-Holland, 2008.
[10] Wesley Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. LFCS, Dept. of Computer Science, University of Edinburgh (January 1, 1992).
[11] Thomas Streicher. Krivine’s Classical Realizability From a Categorical Perspective. Mathematical Structures in Computer Science 23 (6) 1234–1256 (2013).
[12] Thomas Streicher. Realizability Lecture notes of a course given on winter term 2004/05 (Technische Universit ̈at Darmstadt). http://www2.mathematik.tu-darmstadt.de/ streicher/REAL/REAL.pdf
Inscribirse
Ver todos los cursos