From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id EE3B57EE25; Thu, 14 Nov 2013 17:40:54 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Christine.Tasson@pps.univ-paris-diderot.fr) identity=pra; client-ip=194.254.61.138; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Christine.Tasson@pps.univ-paris-diderot.fr"; x-sender="Christine.Tasson@pps.univ-paris-diderot.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Christine.Tasson@pps.univ-paris-diderot.fr) identity=mailfrom; client-ip=194.254.61.138; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Christine.Tasson@pps.univ-paris-diderot.fr"; x-sender="Christine.Tasson@pps.univ-paris-diderot.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@korolev.univ-paris7.fr) identity=helo; client-ip=194.254.61.138; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Christine.Tasson@pps.univ-paris-diderot.fr"; x-sender="postmaster@korolev.univ-paris7.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoUBAHT8hFLC/j2KnGdsb2JhbABagz+DSL1LFg4BAQEBAQgLCQkUKIJPDwEFGyU2AgUWCwILAwIBAgE6EgwGAgKIAa1mkkuBKYxtDoQtgUYDmT+FD4YZiF6BcA X-IPAS-Result: AoUBAHT8hFLC/j2KnGdsb2JhbABagz+DSL1LFg4BAQEBAQgLCQkUKIJPDwEFGyU2AgUWCwILAwIBAgE6EgwGAgKIAa1mkkuBKYxtDoQtgUYDmT+FD4YZiF6BcA X-IronPort-AV: E=Sophos;i="4.93,700,1378850400"; d="scan'208";a="42786940" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 14 Nov 2013 17:40:54 +0100 Received: from mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [81.194.30.253]) by korolev.univ-paris7.fr (8.14.4/8.14.4/relay1/46573) with ESMTP id rAEGeM4g029344; Thu, 14 Nov 2013 17:40:22 +0100 Received: from mailhub.math.univ-paris-diderot.fr (localhost [127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTP id ED9025B174; Thu, 14 Nov 2013 17:40:21 +0100 (CET) X-Virus-Scanned: amavisd-new at math.univ-paris-diderot.fr Received: from mailhub.math.univ-paris-diderot.fr ([127.0.0.1]) by mailhub.math.univ-paris-diderot.fr (mailhub.math.univ-paris-diderot.fr [127.0.0.1]) (amavisd-new, port 10023) with ESMTP id VEMcCF0lOhy6; Thu, 14 Nov 2013 17:40:20 +0100 (CET) Received: from [172.23.36.118] (unknown [172.23.36.118]) (Authenticated sender: tasson) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id 060FE5B17A; Thu, 14 Nov 2013 17:40:20 +0100 (CET) Message-ID: <5284FCF3.3090706@pps.univ-paris-diderot.fr> Date: Thu, 14 Nov 2013 17:40:19 +0100 From: Christine Tasson User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.16) Gecko/20121215 Icedove/3.0.11 MIME-Version: 1.0 To: gdr-im@gdr-im.fr, gdr.gpl@imag.fr, caml-list@inria.fr, coq-club@inria.fr, Why3-club@lists.gforge.inria.fr, frama-c-discuss@lists.gforge.inria.fr Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.2.7 (korolev.univ-paris7.fr [194.254.61.138]); Thu, 14 Nov 2013 17:40:22 +0100 (CET) X-Miltered: at korolev with ID 5284FCF6.000 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 5284FCF6.000 from mailhub.math.univ-paris-diderot.fr/mailhub.math.univ-paris-diderot.fr/null/mailhub.math.univ-paris-diderot.fr/ X-j-chkmail-Score: MSGID : 5284FCF6.000 on korolev.univ-paris7.fr : j-chkmail score : . : R=. U=. O=. B=0.000 -> S=0.000 X-j-chkmail-Status: Ham X-Validation-by: tasson@pps.jussieu.fr Subject: [Caml-list] =?UTF-8?Q?JFLA14_-_Appel_=C3=A0_participation?= *** Appel à participation, merci de diffuser largement *** JFLA'2014 (http://jfla.inria.fr/2014/) Journées Francophones des Langages Applicatifs à Fréjus, du 8 janvier au 11 janvier 2014 Les incriptions aux JFLAs sont désormais ouvertes, veuillez trouver ci-dessous la liste des exposés prévus. Nous espérons que vous serez nombreux à participer à ces journées ; inscrivez-vous dès que possible! Dates importantes ----------------- 15 décembre 2014 : date limite d'inscription aux journées 8 au 11 janvier 2014 : journées Soutien Financier ----------------- Grâce au soutien des GDR GPL et IM et du groupe de travail geocal, nous avons la possibilité de financer une partie des journées pour quelques étudiants ou jeunes chercheurs (date limite de demande le 20 novembre). Cours et exposés invités ------------------------ Olivier Danvy : Du calcul mathématique aux calculs informatiques. Christine Paulin : Modélisation de programme probabilistes en coq. Jean Krivine : Une sémantique pour la biologie moléculaire ? Quelques enjeux (et obstacles) pour l'informatique fondamentale. Xavier Leroy Guillaume Brunerie : HOmotopy Type Theory Catherine Lelay : Coq passe le bac Articles acceptés (par ordre de soumission) ------------------------------------------- Jean-Guillaume Dumas, Dominique Duval, Burak Ekici and Damien Pous. Formal verification in Coq of program properties involving the global state effect Sylvain Conchon, David Declerck, Luc Maranget and Alain Mebsout. Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières Yoichi Hirai and Reynald Affeldt. What could Coq do for Database Software? ---A Progress Report Louis Mandel and Cédric Pasteur. Exécution efficace de programmes ReactiveML Bernard Serpette, Pascal Manoury and Emmanuel Chailloux. Unification des couleurs dans un $\lambda$-calcul polychrome Adrien Husson. Une sémantique statique pour MongoDB Adrien Guatto. Réseaux de Kahn à rafales et horloges entières Martin Bodin, Thomas Jensen and Alan Schmitt. Pretty-big-step-semantics-based Certified Abstract Interpretation Julien Signoles. Comment un chameau peut-il écrire un journal ? Damien Pous and Alan Schmitt. De la KAM avec un Processus d’Ordre Supérieur Marc Bagnol, Amina Doumane and Alexis Saurin. Analyse de dépendances et correction des réseaux de preuve Pierre-Marie Pédrot and Alexis Saurin. Nécessité faite loi : de la réduction linéaire de tête à l'évaluation paresseuse 25 ans des JFLA À l'occasion de ce quart de siècle, les comités de programme et de pilotage ont choisi quatre contributions marquantes parmi les articles publiés aux JFLA ces dix dernières années. Louis Mandel et Marc Pouzet. JFLA'05 ReactiveML, un langage pour la programmation réactive en ML. Sylvain Conchon et Jean-Christophe Filliâtre. JFLA'07 Union-Find Persistant. Sandrine Blazy, Benoît Robillard et Éric Soutif. JFLA'08 Vérification formelle d'un algorithme d'allocation de registres par coloration de graphes. Claude Marché et Asma Tafat. JFLA'13 Calcul de plus faible précondition, revisité en Why3. Comité de programme ------------------- Christine Tasson PPS -- Université Paris Diderot (Présidente) David Baelde LSV -- ÉNS Cachan (Vice président) Jade Alglave University College of London Zaynah Dargaye CEA LIST Jean-Christophe Filliâtre CNRS -- Université Paris Sud Pascal Fradet INRIA Grenoble -- Rhône-Alpes Jacques Garrigue Nagoya University Barbara Petit INRIA Grenoble -- Rhône Alpes Sylvain Pradalier Dassault Systèmes Julien Signoles CEA LIST Matthieu Sozeau INRIA Paris -- Rocquencourt Sylvain Pogodalla Loria/INRIA Nancy Pour tout renseignement d'ordre administratif, contacter -------------------------------------------------------- Sophie Azzaro Inria Grenoble Rhône-Alpes, Bureau des cours et colloques 655 Avenue de l'Europe, Montbonnot 38 334 St Ismier Cedex - France Tel : +33 (0)4 76 61 52 51 - Fax : +33 (0)4 56 52 71 90 email : colloques@inrialpes.fr http://jfla.inria.fr/2014/