Title: Proof transfer for free, beyond type equivalence
Speaker: Assia Mahboubi, INRIA

Abstract: Libraries of formalized mathematics use a possibly broad range of
different representations for a same mathematical concept. Yet light to major
manual input from users remains most often required for obtaining the
corresponding variants of theorems, when such obvious replacements are typically
left implicit on paper. This input represents a significant part of the
bureaucratic work plaguing the activity of writing formal proofs. This issue is
actually specially acute in the context of formally verified computational
mathematics.

In this talk, we propose a novel framework for proof transfer, for proof
assistants based on dependent type theory, such as Lean, Coq or Agda. This
approach relies on original results in type theory, as well as on the design and
implementation of an automation device, which puts them at work on concrete
problems.

This talk will strive to assume little familiarity from the audience with
dependent type theory, explaining in particular all the words in the title, and
trying to illustrate how properties of the foundations backing a proof assistant
may impact the practice of formalizing mathematics.

This is a joint work with Enzo Crance and Cyril Cohen.