BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Departamento de Computación - ECPv6.15.18//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
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:20200101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=America/Sao_Paulo:20211105T140000
DTEND;TZID=America/Sao_Paulo:20211105T150000
DTSTAMP:20260502T225316
CREATED:20211027T153308Z
LAST-MODIFIED:20211027T153308Z
UID:7125-1636120800-1636124400@www.dc.uba.ar
SUMMARY:Defensa Tesis Licenciatura Teodoro Freund
DESCRIPTION:Título: «PRK\, una lógica constructiva clásica»\nDirector: Pablo Barenbaum\nJurado:\n– Eduardo Bonelli (Stevens Institute of Technology)\n– Santiago Figueira (ICC\, CONICET) \nResumen: \nEsta tesis presenta el sistema PRK\, un sistema lógico en el cual las\nnociones de prueba y refutación son duales. Este sistema extiende a la\nlógica clásica y es constructivo en el sentido de que se lo puede\ndotar de una interpretación computacional con buenas propiedades. Las\nfórmulas de PRK se clasifican a lo largo de dos ejes\, dependiendo de\nsu positividad (afirmación o negación) y su fuerza (fuerte o clásica).\nLas proposiciones fuertes se demuestran\, canónicamente\, con reglas de\nintroducción\, mientras que las proposiciones clásicas se demuestran\npor reducción al absurdo. El sistema PRK resulta ser correcto y\ncompleto con respecto a una clase de modelos de Kripke\, definida en\neste mismo trabajo. Siguiendo la correspondencia de Curry–Howard\, se\nformaliza un cálculo asociado a PRK\, denominado λPRK\, cuyo sistema de\ntipos se corresponde con el sistema lógico PRK. Se establecen varias\npropiedades sobre λPRK\, incluyendo preservación de tipos\, confluencia\ny una caracterización de las formas normales de las pruebas y\nrefutaciones. La terminación fuerte del cálculo λPRK se demuestra a\ntravés de una traducción a System F extendido con ecuaciones\nrecursivas entre tipos\, y apoyándose en un resultado de Mendler. Por\núltimo\, se considera una extensión a segundo orden del sistema PRK\,\njunto con el cálculo correspondiente λPRK2. Se extienden a este marco\nlos resultados anteriormente mencionados\, exceptuando la terminación\nfuerte de λPRK2\, que queda abierta como trabajo futuro.
URL:https://www.dc.uba.ar/event/defensa-tesis-licenciatura-teodoro-freund/
LOCATION:Youtube
CATEGORIES:Agenda
END:VEVENT
END:VCALENDAR