Concept alignment in Logipedia

Logipedia is an on line encyclopedia of formal proofs, in various
theories expressed in the lambda-Pi-calculus modulo theory. When a
user downloads a proof from Logipedia to her own system, she does not
want to redefine the basic concepts, such as the notions of natural
number or of addition, but instantiate the Logipedia concepts with
those of her own system, that is see a proof as a functor that applies
to a set of definitions.

Advisor: Gilles Dowek

Bibliography: T. Zimmermann and H.  Herbelin, Automatic and
Transparent Transfer of Theorems along Isomorphisms in the Coq Proof
Assistant. CICM 2015.