Sites Inria

Conférence scientifique

Séminaire Calculs et preuves, organisé par l'équipe SpecFun

© INRIA Sophie Auvin - S comme Simulation

  • Date : 6/03/2017
  • Lieu : Inria Saclay - Île-de-France 1 rue Honoré d'Estienne d'Orves Bâtiment Alan Turing Campus de l'École Polytechnique 91120 Palaiseau

L'équipe-projet SpecFun du centre de recherche Inria Saclay - Île-de-France organise le mardi 6 mars, à 10h30, un séminaire "Calculs et preuves" au Bâtiment Alan Turing à Palaiseau, siège du centre de recherche Inria Saclay - Île-de-France.

Damien Rouhling y fera un exposé sur « Refinement : a reflection on proofs and computations ».

Abstract :

"Modern proof assistants have to deal with problems of increasing complexity and rely more and more on computation to automate proofs. However, efficient algorithms are usually complex and the proof of their soundness often requires the formalization of advanced mathematics. This creates a tension between efficiency and ease of proof.  We will present a framework originally designed for algebra and allowing to deal with both aspects separately. This framework makes it possible both to prove more easily the soundness of complex algorithms and to use them to automate proofs. We will then focus on insights this framework gave us into the design of computation-based proof procedures."

Mots-clés : Inria Saclay – Île-de-France SpecFun

Haut de page

Suivez Inria