Defensa de tesis de doctorado de Pablo Barenbaum

Defensa de tesis de doctorado

Pablo Barenbaum

Fecha: viernes 20 de noviembre de 2020.

Hora: 16:00 (GMT-3, hora argentina).

Link:

https://www.youtube.com/watch?v=uwzgFrOabNQ

Título

Semántica dinámica de cálculos de sustituciones explícitas a distancia

Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires

Directores

Eduardo Bonelli (Stevens Institute of Technology)
Delia Kesner (IRIF, Université de Paris; Institut Universitaire de France)

Jurado

Nazareno Aguirre (Universidad Nacional de Río Cuarto; CONICET)
Zena Ariola (University of Oregon)
Alexandre Miquel (IMERL, Fing, Universidad de la República)

Resumen

Los cálculos de sustituciones explícitas son variantes del cálculo-λ en los que la operación de sustitución no se define a nivel del metalenguaje, sino con reglas de reescritura que la implementan. Nuestro principal objeto de estudio es un cálculo de sustituciones explícitas particular, el Linear Substitution Calculus (LSC), definido por Accattoli y Kesner en 2010. Se caracteriza por el hecho de que las reglas de reescritura operan no localmente (a distancia). En esta tesis, en primer lugar, definimos máquinas abstractas que implementan estrategias de evaluación en el LSC: call-by-name para evaluación débil y fuerte, call-by-value y call-by-need. Demostramos que dichas máquinas son correctas y preservan la complejidad temporal. En segundo lugar, definimos una extensión de la estrategia de evaluación call-by-need en el LSC para evaluación fuerte. Demostramos que la estrategia es completa con respecto a call-by-name, usando un sistema de tipos intersección no idempotente, y mostramos cómo extenderla para lidiar con pattern matching y recursión. Por último, estudiamos la teoría de residuos y familias de radicales en el LSC. Para ello definimos una variante del LSC con etiquetas de Lévy, lo que nos permite demostrar que cumple con la propiedad de Finite Family Developments. Aplicamos esta propiedad para obtener resultados de optimalidad, estandarización y normalización de estrategias en el LSC, y generalizamos algunos de estos resultados al marco axiomático de Deterministic Family Structures.