From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q0JHGTGQ024399 for ; Thu, 19 Jan 2012 18:16:29 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aj0CADtPGE/RVdI2kGdsb2JhbABErF94CCIBAQEBCQkNBxQEIYFzAQEEDAYCLAESHwgDDAEFEDsiEgEFAQYWBgESGweHYpt5Co5ZhQqJMAIFC4hxAQEDAQECBQECAgEBAQEBAQIBAQMBAQEEBAICAgEBAgECAQILCRQJBQEFAg4GBTUFBwELAQIBAQgBAQGDCIQcBJUXiwODDD2BT4Iw X-IronPort-AV: E=Sophos;i="4.71,537,1320620400"; d="scan'208";a="128119717" Received: from mail-pz0-f54.google.com ([209.85.210.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 19 Jan 2012 18:16:27 +0100 Received: by dadi14 with SMTP id i14so137906dad.27 for ; Thu, 19 Jan 2012 09:16:25 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type :content-transfer-encoding; bh=WQ07qAfKfIlE5bTjjILCzTQVluv1LxROtHzeVIwjDxw=; b=duO0REDi4t8au4mZJNGbwUaoo1ZxtOzgAcBYSUQUErLIReg3T2Q1t0HH1ap7VBu7dv JZAuUCc8Ljn8vFOIpnBmQPPaxWswUrEVPW6y3oMjD6RQ4wUv5yneTfJK2FXLYGoQrxP3 VALOi3keJHSRBWeR12ZSejlx7fYYajp6hokOg= MIME-Version: 1.0 Received: by 10.68.115.40 with SMTP id jl8mr53756227pbb.94.1326993385727; Thu, 19 Jan 2012 09:16:25 -0800 (PST) Sender: damien.pous@gmail.com Received: by 10.142.204.20 with HTTP; Thu, 19 Jan 2012 09:16:25 -0800 (PST) In-Reply-To: <4F17D43F.60301@inria.fr> References: <4F17D43F.60301@inria.fr> Date: Thu, 19 Jan 2012 18:16:25 +0100 X-Google-Sender-Auth: lcFf7CeU9i4SMG0mnjxGwM8a_3w Message-ID: From: Damien Pous To: caml-list , gdr-im Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q0JHGTGQ024399 Subject: [Caml-list] JFLA 2012 [ 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 symposia@inria.fr. 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