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.