BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Alfredo Álzaga (Universidad Nacional del Sur)
DTSTART:20210514T170000Z
DTEND:20210514T180000Z
DTSTAMP:20260423T021708Z
UID:SemACT/16
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/SemACT/16/">
 Dependent Type Theory - Una Introducción</a>\nby Alfredo Álzaga (Univers
 idad Nacional del Sur) as part of Seminario de álgebra\, combinatoria y t
 eoría de Lie\n\n\nAbstract\nEstos sistemas utilizan la correspondencia Cu
 rry-Howard para integrar la computación y la lógica. Sirven para fundame
 ntar la matemática y son utilizados como base por proof assitants como\, 
 por ejemplo Nuprl\, Coq\, Lean o Agda.\n\nEn esta charla mostraremos los m
 ecanismos básicos de este tipo de lógicas.\n
LOCATION:https://researchseminars.org/talk/SemACT/16/
END:VEVENT
END:VCALENDAR