BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Departamento de Computación - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Departamento de Computación
X-ORIGINAL-URL:https://www.dc.uba.ar
X-WR-CALDESC:Eventos para Departamento de Computación
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:America/Sao_Paulo
BEGIN:STANDARD
TZOFFSETFROM:-0200
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20190217T020000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20201120T160000
DTEND;TZID=America/Sao_Paulo:20201120T180000
DTSTAMP:20260517T092239
CREATED:20201118T151027Z
LAST-MODIFIED:20201118T151027Z
UID:6434-1605888000-1605895200@www.dc.uba.ar
SUMMARY:Defensa Tesis Doctorado Pablo Barenbaum
DESCRIPTION:Título: Semántica dinámica de cálculos de sustituciones explícitas a distancia \nDirectores: Eduardo Bonelli y Delia Kesner. \nJurados:\nDr. Nazareno Aguirre (Universidad de Río Cuarto y CONICET)\nDr. Zena Ariola (University of Oregon)\nDr. Alexandre Miquel (Universidad de la República / Fing / IMERL) \nResumen:\nLos cálculos de sustituciones explícitas son variantes del cálculo-lambda 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.
URL:https://www.dc.uba.ar/event/defensa-tesis-doctorado-pablo-barenbaum/
LOCATION:ZOOM
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR