Proof Synthesis with Free Extensions in Intensional Type Theory

Add to your list(s) Download to your calendar using vCal

• Nathan Corbyn (University of Cambridge)
• Friday 18 June 2021, 11:00-12:00
• https://meet.google.com/jxy-edcv-wgx.

If you have a question about this talk, please contact Nathanael Arkor.

Recent developments in the foundations of mathematics have led to a surge of interest in intensional theories of types and their applications in verified programming & formalised mathematics. Due to their constructive nature, these theories generally cannot benefit from classical proof automation techniques, 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 burden. Ultimately, I’ll describe an extensible tactic that I’ve developed for the Agda proof assistant, capable of synthesising proofs of algebraic identities. This tactic is formally verified as sound and complete, does not rely on postulates or extensionality, and is compatible with a broad variety of Agda configurations.

This talk is part of the Logic & Semantics for Dummies series.

This talk is included in these lists:

• Logic & Semantics for Dummies
• https://meet.google.com/jxy-edcv-wgx
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.