BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proof Synthesis with Free Extensions in Intensional Type Theory - 
 Nathan Corbyn (University of Cambridge)
DTSTART:20210618T100000Z
DTEND:20210618T110000Z
UID:TALK160795@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:Recent developments in the foundations of mathematics have led
  to a surge of interest in intensional theories of types and their applica
 tions in verified programming & formalised mathematics. Due to their const
 ructive nature\, these theories generally cannot benefit from classical pr
 oof automation techniques\, but concurrently require a great deal of ‘bo
 okkeeping’ to work with their proof-relevant notions of identity. In thi
 s talk\, I’ll discuss a family of constructions know as ‘free extensio
 ns’ and how they can help alleviate some of this burden. Ultimately\, I
 ’ll describe an extensible tactic that I’ve developed for the Agda pro
 of assistant\, capable of synthesising proofs of algebraic identities. Thi
 s tactic is formally verified as sound and complete\, does not rely on pos
 tulates or extensionality\, and is compatible with a broad variety of Agda
  configurations.
LOCATION:https://meet.google.com/jxy-edcv-wgx
END:VEVENT
END:VCALENDAR