Séminaire GT UPSCaLe

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.