People:
Olivier Hermant, Richard Bonichon, Alberto Naibo, Chantal Keller, Paul Brauner, Benjamin Werner, Claude Kirchner,
Mathieu Boespflug, Denis Cousineau, Gilles Dowek, Cody Roux, Lisa Allali, Clément Houtmann, Guillaume Burel,
Maxime, Pierre, Aloïs.
Mathieu Boespflug, Denis Cousineau, Gilles Dowek, Cody Roux, Lisa Allali, Clément Houtmann, Guillaume Burel,
Maxime, Pierre, Aloïs.
Schedule:
- 09h30-11h30: Towards a prover based on deduction modulo, Guillaume Burel (⇾ get slides)
- 11h30-12h45: Dedukti: pattern matching and termination, Cody Roux (⇾ get article)
- 14h15-15h30: Normalization in lambda-Pi modulo and proof representation of HOL proofs in Dedukti, Gilles Dowek
- 15h30-16h00: 3-dimensional proof nets for classical logic, Clément Houtmann (⇾ get article)
- 16h00-17h00: Transforming pre-models into models, Olivier Hermant (⇾ get slides)
- 17h00-18h00: Business meeting
