[ This message is intentionally written in French ] Ultime appel à participation
JFLA'2012 (http://jfla.inria.fr/2012/) Journées Francophones des Langages Applicatifs 4 février au 7 février 2012, Carnac Vous pouvez encore vous inscrire aux JFLA 2012 jusqu'à demain! La page d'inscription est disponible sur le site http://jfla.inria.fr/2012/. L'édition 2012 des Journées Francophones des Langages Applicatifs aura lieu à Carnac du 4 février à 15h au 7 février 2012 à midi. Pour tout renseignement, contacter [email protected]. Les journées des 4 et 5 février seront consacrés aux cours invités de Jean-Christophe Filliâtre (LRI, Cnrs) et Matthieu Sozeau (Inria). Les journées des 6 et 7 février seront consacrés aux exposés présentant les articles sélectionnes ainsi qu'aux exposés des orateurs invités Benjamin Grégoire (Inria) et Dimitrios Vytiniotis (Microsoft Research). La liste des articles acceptés est disponible ici: http://jfla.inria.fr/articles_acceptes_2012.html A bientôt à Carnac, Assia Mahboubi et Damien Pous *Cours Invités* Jean-Christophe Filliâtre : Vérification déductive de programmes avec Why3 Ce cours est une introduction à la preuve de programmes en général, et à l'outil Why3 en particulier (http://why3.lri.fr/). L'outil Why3 permet d'écrire des programmes dans un langage très proche d'OCaml (polymorphisme, types algébriques, filtrage, exceptions, références, tableaux, etc.), de leur donner une spécification dans une logique du premier ordre, et de prouver leur correction à l'aide de démonstrateurs interactifs ou automatiques (Coq, Alt-Ergo, Z3, CVC3, etc.). Au travers de nombreux exemples, ce cours introduit des concepts élémentaires de preuve de programmes (pré- et postcondition, invariant de boucle, variant) mais aussi des techniques (spécification, preuve de terminaison, modélisation de structures de données). Matthieu Sozeau : Classes de types en Coq Nous présentons dans ce cours une extension légère à Coq permettant de faire des développements génériques via un mécanisme de surcharge inspiré d’Haskell. Sans modifier le langage primitif du calcul des constructions, les classes donnent à l’utilisateur des facilités de haut niveau pour travailler avec des structures abstraites tout en permettant leur instanciation efficace sur des structures concrètes. Il permet aussi d’ajouter de l’intelligence au système en étendant l’algorithme de typage, lui permettant de trouver par résolution un habitant d’une classe donnée. Ce principe de surchage s’étend naturellement à l’environnement tout entier, en particulier au système de tactiques de Coq. Nous présenterons tout d’abord le fonctionnement basique du système de classes implémenté dans Coq (et disponible depuis la version 8.2) puis son utilisation pratique au cours d’un tutoriel. Nous introduirons progressivement différents raffinements rendant le système plus agréable à l’usage. *Exposés Invités* Benjamin Grégoire : Easycrypt : un outil pour les preuves de cryptographie exacte Après une rapide introduction des notions de cryptographie exacte, je présenterai la notion de preuve par réduction qui est une méthodologie couramment utilisée par les cryptographes pour établir la correction et la sécurité de primitives cryptographiques telles que Elgamal ou OAEP. Je présenterai ensuite les différentes notions qui ont permis de développer Certicrypt (une librairie Coq permettant de formaliser la sécurité de primitives cryptographiques), en mettant un accent particulier sur la logique pRHL (probabilistic Relationnal Hoare Logic). J'illustrerai ensuite ces notions sur un exemple simple : la sécurité sémantique de Elgamal. Je finirais l'exposé avec la présentation d'un nouvel outil (Easycrypt) qui réutilise les concepts mis en place dans Certicrypt mais repose sur une utilisation intensive de prouveurs automatiques tels que alt-ergo, z3, ou vampire. Dimitrios Vytiniotis : Stop when you are Almost-Full: terminator and size-change termination in Coq [joint work with Thierry Coquand] Disjunctive well-foundedness (as used for instance in the Terminator tools), size-change termination, and well-quasi-orders (used in term-rewrite systems) are examples of techniques that have been successfully applied to automatic proofs of program termination and online termination testing, respectively. Although these works originate in different communities, there is an intimate connection between them - they rely on closely related principles and employ similar arguments from Ramsey theory. At the same timethere is a notable absence of these techniques in programming systems based on constructive type theory. In this talk we will explain the aforementioned connection and present some novel tools to perform induction in Coq, inspired from that large body of previous work. The benefit is nice composability properties of termination arguments at the cost of intuitive and lightweight user obligations. Inevitably, we have to present some Ramsey-like arguments: Though similar proofs are typically classical, we offer an entirely constructive development standing on the shoulders of Veldman and Bezem, and Richman and Stolzenberg. This work is to our knowledge the first constructive justification of Terminator and Size-Change termination and opens the way towards employing these techniques, without any further logical assumptions, in Coq. *Articles acceptés* Simon Boulier et Alan Schmitt : Formalisation de HOCore en Coq Pierre Boutillier : Ad hoc reductions make structural guard condition stricter and smarter Cyril Cohen : Construction des nombres algébriques réels en Coq Christophe Deleuze : Concurrence et continuations en OCaml Jean-François Durfourd : Dérivation de l'algorithme de Schorr-Waite en Coq par une méthode algébrique Fabrice Le Fessant et Thomas Gazagnaire : Gestion de projet avec ocp-build Mathieu Jaume et Renaud Rioboo : Développement de systèmes sécurisés avec l'atelier FoCaLiZe Catherine Lelay et Guillaume Melquiond : Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert Daniel De Rauglaudre : Vérification formelle de conditions d'ordonnancabilité de tâches temps réel périodiques strictes Bernard Serpette et Emmanuel Chailloux : Séparation des couleurs dans un lambda-calcul bichrome -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
