Classical proofs in Logipedia
Logipedia is an on line encyclopedia of formal proofs, in various
theories expressed in the lambda-Pi-calculus modulo theory. The goal
of this internship is to define classical connectors and quantifiers
in the lambda-Pi-calculus modulo theory to include classical proofs in
Logipedia. The practical goal is to include in Logipedia the standard
library of HOL Light, that has already been translated in Dedukti.
Advisor: Gilles Dowek
Bibliography: G. Dowek, On the definition of the classical
connectives and quantifiers, E.H. Haeusler, W. de Campos Sanz, and
B. Lopes (eds.) Why is this a Proof?, Festschrift for Luiz Carlos
Pereira, College Publications, 2015.