Programme:

10h00-111h30 Maxime Denes: Compilation native et structures primitives

11h30-12h30 Alois Brunel: Candidats de réductibilité quantitatifs et logiques
light modulo

14h-14h45 Chantal Keller: Encoding HOL into Dedukti

14h45-15h30 Cody Roux dependent types as higher order dependency pairs

15h30-16h Olivier Hermant: Generalizing Boolean Algebras for Deduction Modulo(⇾ get slides)

16h-16h45 Clément Houtmann: Superdeduction, Focusing and Pattern Matching
(work in progress)

16h45 -17h Clément Houtmann Checking LKF proofs using Dedukti

17h discussions