Guillermo González, Mauricio Germán

Investigo acerca de los Juegos en Realizabilidad Clásica –la teoría de juegos es un modelo teórico de la programación interactiva– asociados a las fórmulas de la aritmética de orden superior. Las demostraciones tienen asociados $\lambda_c$-términos –i.e.: programas en un lambda cálculo extendido con instrucciones de control–. Mi trabajo está orientado a la descripción operativa de las estrategias ganadoras implementadas por los $\lambda_C$-t\’erminos asociados a una demostración.

La teoría general dice que, en la aritmética de orden superior –sistema de tipos
de $\lambda_C$–, el $\lambda_C$-término asociado a
una demostraci\’on de una implicación es capaz de
combinar estrategias ganadoras para los juegos asociados a las
hipótesis para obtener una estrategia ganadora para el juego
asociado a la conclusión. Comprender como las demostraciones actúan como combinadores de estrategias es fundamental en la Semántica de Juegos, ya que establece un significado algorítmico de las demostraciones.

Otro problema relevante es el Problema de la Especificación, el cual consiste en hallar una caracterización algorítmica para los realizadores de una fórmula dada. Esta caracterización se
describe en términos de la Teoría de Juegos.