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:-0300
TZOFFSETTO:-0300
TZNAME:-03
DTSTART:20230101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20240221T180000
DTEND;TZID=America/Sao_Paulo:20240221T190000
DTSTAMP:20260408T012218
CREATED:20240214T125354Z
LAST-MODIFIED:20240219T121556Z
UID:8891-1708538400-1708542000@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Giselle Zeitoune
DESCRIPTION:Título: Un cálculo-lambda cronometrado\nDirector: Pablo Barenbaum\nJurado: Sergio Abriola y Rafael Romero \nResumen:\nEl cálculo-lambda permite estudiar la noción de función computable desde un\npunto de vista matemático\, modelando la abstracción y la aplicación de una\nfunción a un argumento. El mecanismo de cómputo por el cual se realiza esta\naplicación se conoce como beta-reducción. En este trabajo extendemos el\ncálculo-lambda a una variante «cronometrada»\, a la que llamamos cálculo-lambda\ncronometrado. Extendemos la sintaxis\, la semántica y el sistema de tipos para\nreflejar el hecho de que la aplicación de una función a un argumento tiene un\ncosto temporal. Para esto se incorpora un constructor de términos que\nrepresenta una demora de una unidad de tiempo\, y un operador que modela la\nacción de esperar hasta que el resultado de un cómputo esté listo. Modificamos\nel mecanismo de cómputo para que cada paso de beta-reducción introduzca una\ndemora. Demostramos que este cálculo preserva propiedades como la confluencia y\nla normalización fuerte del fragmento tipado. Damos un argumento de terminación\ndébil\, bajo ciertas hipótesis de tipabilidad\, que exhibe una cota explícita\npara la longitud de la reducción a forma normal\, basado en las características\ndel nuevo cálculo\, usando la noción de costo definida. Finalmente\, demostramos\nque hay términos tipables en el cálculo-lambda a los que no se les puede hacer\ncorresponder un término tipable en el cálculo-lambda cronometrado. Este\nresultado se obtiene por medio de un sistema de tipos auxiliar en el que los\njuicios de tipado vienen acompañados de restricciones ecuacionales.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-giselle-zeitoune/
LOCATION:Aula 1114
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR