From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id EEDDC7EE99; Mon, 9 Dec 2013 12:25:27 +0100 (CET) Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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: AgAEAAOopVLC/j2KgWdsb2JhbABZgz+DUrdAFg4BAQsLCQcUKoJPDwEFGyU2AgUWCwILAwIBAgE6EgwGAgKIAqlsiAaPNYEpjQUOAwGDQoFIA5lEhRWGGIhggXA X-IPAS-Result: AgAEAAOopVLC/j2KgWdsb2JhbABZgz+DUrdAFg4BAQsLCQcUKoJPDwEFGyU2AgUWCwILAwIBAgE6EgwGAgKIAqlsiAaPNYEpjQUOAwGDQoFIA5lEhRWGGIhggXA X-IronPort-AV: E=Sophos;i="4.93,857,1378850400"; d="scan'208";a="40032415" Received: from korolev.univ-paris7.fr ([194.254.61.138]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 09 Dec 2013 12:25:27 +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 rB9BOscu005239; Mon, 9 Dec 2013 12:24:54 +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 58F466D628; Mon, 9 Dec 2013 12:24:54 +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 jxk5u3z1ayOU; Mon, 9 Dec 2013 12:24:52 +0100 (CET) Received: from [172.23.36.57] (unknown [172.23.36.57]) (Authenticated sender: tasson) by mailhub.math.univ-paris-diderot.fr (Postfix) with ESMTPSA id 071756D615; Mon, 9 Dec 2013 12:24:51 +0100 (CET) Message-ID: <52A5A883.2030001@pps.univ-paris-diderot.fr> Date: Mon, 09 Dec 2013 12:24:51 +0100 From: Christine Tasson Reply-To: Christine.Tasson@pps.univ-paris-diderot.fr User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20131103 Icedove/17.0.10 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]); Mon, 09 Dec 2013 12:24:54 +0100 (CET) X-Miltered: at korolev with ID 52A5A886.001 by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 52A5A886.001 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 : 52A5A886.001 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: christine.tasson@pps.univ-paris-diderot.fr Subject: [Caml-list] =?UTF-8?Q?JFLA14_-_Dernier_appel_=C3=A0_participation?= *** Appel à participation, Date limite d'inscription 15/12 *** 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 bientôt closes, veuillez trouver ci-dessous la liste des exposés prévus. Nous espérons que vous serez nombreux à participer à ces journées ! Dates importantes ----------------- 15 décembre 2014 : date limite d'inscription aux journées 8 au 11 janvier 2014 : journées 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/