To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 07/09/07 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Vendredi 7 septembre, 10h30 ------------ David Baelde ------------ INRIA & LIX, École Polytechnique ======================================================== Model-checking sur des théories avec liaison de variable ======================================================== Bedwyr est un outil de programmation logique qui permet de calculer et de vérifier des propriétés de type "model-checking" sur des structures syntaxiques avec liaison de variable. Il repose sur la logique LINC, une extension de la logique intuitionniste dont les deux composantes essentielles sont reflétées dans Bedwyr: (1) D'abord, la notion de définition permet de formaliser symétriquement succès et échec (finis) de la recherche de preuve. Cela permet de capturer proprement la négation en programmation logique. On modélise ainsi aussi bien may- et must-behavior dans les spécifications de sémantique opérationnelle. (2) La syntaxe abstraite d'ordre supérieur (HOAS) est supportée au niveau logique par la présence de termes d'ordre supérieur et le quantificateur nabla, et l'unification des higher-order patterns dans l'implémentation. Ceci permet de raisonner directement sur des expressions comportant des liaisons de variable. Bedwyr est un logiciel libre disponible sur [1]. La distribution comprend de nombreux exemples, dont plusieurs variantes du pi-calcul (sémantique opérationnelle, bisimulation, analyse de traces, logiques modales), lambda-calcul, stratégies gagnantes dans des jeux, etc. Je commencerai par présenter brièvement la logique LINC et la méthodologie de formalisation associée. Je montrerai ensuite comment Bedwyr exploite ces avancées en théorie de la démonstration. Pour finir j'aborderai quelques points intéressants relatifs à l'implémentation de ce système en OCaml. [1]