--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on March 2010 ---
Dear Frama-C users, Sorry about this message in French, but its purpose is to announce lessons about the COQ system that will be given in French anyway. If you don't speak French and are still interested about that, there will be similar lessons in English in China in August. You can also have a look at this introduction : http://hal.inria.fr/inria-00001173 -------------------------------------------------- Ecole CEA-EDF-INRIA "Mod?lisation et v?rification d'algorithmes en Coq : une introduction" Paris, 7-11 juin 2010, http://www.inria.fr/ecoles-cea-edf-inria Le syst?me Coq fournit un langage de programmation fonctionnelle et un cadre de raisonnement pour effectuer des preuves sur les programmes. Le pouvoir expressif du langage est suffisant pour d?crire des logiciels aussi puissants que des compilateurs et faire des preuves math?matiques aussi difficiles que le th?or?me des quatre couleurs. Dans cette ?cole nous abordons les techniques de programmation et de preuve de fa?on pragmatique et progressive. Les sujets abord?s sont : - programmation r?cursive - manipulations de listes et d'entiers - d?monstration par r?currence - d?finition de nouveaux types de donn?es - programmation par filtrage et raisonnement par cas - propri?t?s inductives -------------------------------------------------- -- Anne Pacalet : http://www-sop.inria.fr/members/Anne.Pacalet/