BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//SECURITY & APPLIED LOGIC - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:SECURITY & APPLIED LOGIC
X-ORIGINAL-URL:https://sal.cs.unibuc.ro
X-WR-CALDESC:Events for SECURITY & APPLIED LOGIC
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Bucharest
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20200329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20201025T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20210328T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20211031T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20220327T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20221030T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Bucharest:20210225T100000
DTEND;TZID=Europe/Bucharest:20210225T120000
DTSTAMP:20260423T094452
CREATED:20210224T154805Z
LAST-MODIFIED:20210317T164757Z
UID:687-1614247200-1614254400@sal.cs.unibuc.ro
SUMMARY:Formalizing Gödel's System T in Lean
DESCRIPTION:Title: Formalizing Gödel’s System T in Lean \nSpeaker: Horațiu Cheval (University of Bucharest)  \n\nAbstract: \n\nIn 1958\, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory\, notably the program of proof mining. We give a brief overview of Gödel’s System T and then explore a formalization thereof as a deep embedding in the Lean proof assistant. \nReferences: \n\n[1] mathlib Community\, The Lean Mathematical Library\, 2019.
URL:https://sal.cs.unibuc.ro/event/formalizing-go%cc%88dels-system-t-in-lean/
CATEGORIES:Logic Seminar
END:VEVENT
END:VCALENDAR