University of Cambridge > Talks.cam > Logic & Semantics for Dummies > Proof Synthesis with Free Extensions in Intensional Type Theory

Proof Synthesis with Free Extensions in Intensional Type Theory

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity