SAVE THE DATE
Scientific day – GT UPScale
Tuesday, October 9, 2018
Interoperability Of Proof Systems
LRI – Paris-Sud University – Shannon auditorium – building 660.
This seminar will present various projects around interoperability of proof systems:
- 09:00 – 09:30 : welcome coffee
- 09:30 – 09:40 : Chantal Keller, opening
- 09:40 – 10:40 : Cezary Kaliszyk, “Reinforcement Learning of Theorem Proving”
- 10:40 – 11:10 : break
- 11:10 – 11:55 : François Pessaux, “Programming and proving with FoCaLiZe: a tour from computer algebra to interoperability applications” – joined work with Catherine Dubois
- 11:55 – 12:40 : Guillaume Burel, “Bridging holes on Dedukti proofs, an overview”
- 12:40 – 14:00 : buffet
- 14:00 – 14:45 : Dale Miller, “Formal proof and trust”
- 14:45 – 15:45 : Florian Rabe and Gilles Dowek, “Shared background library”
- 15:45 – 16:15 : break
- 16:15 – 17:00 : Stéphane Graham-Lengrand, “Proving theorems with quantifier elimination techniques”
Cezary Kaliszyk (University of Innsbruck, Austria) will be our guest.