BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &\; Semantics for Dummies
SUMMARY:Proof Synthesis with Free Extensions in Intensiona
l Type Theory - Nathan Corbyn (University of Cambr
idge)
DTSTART;TZID=Europe/London:20210618T110000
DTEND;TZID=Europe/London:20210618T120000
UID:TALK160795AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/160795
DESCRIPTION:Recent developments in the foundations of mathemat
ics have led to a surge of interest in intensional
theories of types and their applications in verif
ied programming & formalised mathematics. Due to t
heir constructive nature\, these theories generall
y cannot benefit from classical proof automation t
echniques\, but concurrently require a great deal
of ‘bookkeeping’ to work with their proof-relevant
notions of identity. In this talk\, I’ll discuss
a family of constructions know as ‘free extensions
’ and how they can help alleviate some of this bur
den. Ultimately\, I’ll describe an extensible tact
ic that I’ve developed for the Agda proof assistan
t\, capable of synthesising proofs of algebraic id
entities. This tactic is formally verified as soun
d and complete\, does not rely on postulates or ex
tensionality\, and is compatible with a broad vari
ety of Agda configurations.
LOCATION:https://meet.google.com/jxy-edcv-wgx
CONTACT:Nathanael Arkor
END:VEVENT
END:VCALENDAR