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.