Logipedia Kick off meeting

21-23 January 2019, LSV, Building Laplace

Left to right: Claude Kirchner, Hande Gözükan, Rob Lewis, Cezary Kaliszyk, Romain Primet, Georges Gonthier, Hugo Herbelin, Burkhart Wolff, Julien Narboux, Jean-Pierre Jouannaud, Claudio Sacerdoti Coen, Pierre-Yves Strub, Jean-Daniel Fekete, Catherine Dubois, Thibault Gauthier, Théo Zimmermann, Olivier Hermant, Pierre Senellart, Emilio Gallego Arias, Frédéric Blanqui, Pierre Boutry, Cyril Cohen, Yacine El Haddad, Gilles Dowek, Denis Cousineau, Guillaume Genestier, François Thiré, Valentin Blot, Franck Slama, Gaspard Férey, Farzad Jafarrahmani, Emilie Grienenberger, and Guillaume Burel. Not on the photo: Raphaël Cauderlier, Stéphane Demri, Chantal Keller, Dale Miller, and Karol Pąk.

Program:

• Monday morning: Presentation of Logipedia (Gilles Dowek) + discussion
• Monday afternoon: Translating Logipedia proofs from one theory to another and exporting them to different systems (François Thiré) + discussion
• Monday evening: Break out sessions
• Tuesday morning: Translating proofs from an existing library to Logipedia (Chantal Keller) + discussion
• Tuesday afternoon: Concept alignment: how to use Logipedia proofs in my system? Alignments and Their Applications (Cezary Kaliszyk) and Theorem and proof transfer for a universal collaborative repository of formal proofs (Théo Zimermann) + discussion
• Tuesday evening: Break out sessions
• Wednesday morning: Translating proofs from automated theorem provers to Logipedia (Guillaume Burel) + discussion