Abstract
As is the case in the literature, the addition of a mathematical concept to a corpus of formal libraries typically gives rise to several variants of definitions, most often equivalent but not always. Unfortunately, transposing the formal theorem provers associated with these different variants is then very pedestrian, whereas on paper, these trivial steps would remain implicit. This necessary bureaucracy is in fact a notorious brake on the formalization of "interesting" mathematics. In this talk, we will discuss the construction of a type-theoretic proof transfer tool. Based on a generalization of the Tabareau-Tanter-Sozeau parametricity translation, this approach can be used in provers such as Rocq or Lean. This work is in collaboration with Cyril Cohen and Enzo Crance.
Assia Mahboubi
Assia Mahboubi is Director of Research at Inria, in the Nantes Digital Science Laboratory. She also holds a chair in the Mathematics Department of the Vrije Universiteit Amsterdam, in the Netherlands.
