From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.7 required=5.0 tests=AWL,SPF_SOFTFAIL autolearn=disabled version=3.1.3 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 2CC81BC6B for ; Wed, 9 Jan 2008 16:41:47 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABZ6hEfAXQInh2dsb2JhbACQHAEBAQgKKZkp X-IronPort-AV: E=Sophos;i="4.24,263,1196636400"; d="scan'208";a="7608158" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 09 Jan 2008 16:41:46 +0100 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m09FfcSF002347 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Wed, 9 Jan 2008 16:41:46 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABZ6hEfUGypAimdsb2JhbACQHAEBAQgEBiIHmSk X-IronPort-AV: E=Sophos;i="4.24,263,1196636400"; d="scan'208";a="5874946" Received: from smtp7-g19.free.fr ([212.27.42.64]) by mail2-smtp-roc.national.inria.fr with ESMTP; 09 Jan 2008 16:41:46 +0100 Received: from smtp7-g19.free.fr (localhost [127.0.0.1]) by smtp7-g19.free.fr (Postfix) with ESMTP id 071E1322823; Wed, 9 Jan 2008 16:41:46 +0100 (CET) Received: from [192.168.0.1] (sgc91-2-82-237-76-251.fbx.proxad.net [82.237.76.251]) by smtp7-g19.free.fr (Postfix) with ESMTP id C93F1322814; Wed, 9 Jan 2008 16:41:45 +0100 (CET) Mime-Version: 1.0 (Apple Message framework v753) Content-Transfer-Encoding: quoted-printable Message-Id: <03DDC185-8DDF-4AE3-B6F0-BBFCFDA9D525@ensiie.fr> Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed To: caml-list@inria.fr, coq-club@pauillac.inria.fr From: Sandrine Blazy Subject: =?ISO-8859-1?Q?JFLA2008:_2e_appel_=E0_participation?= Date: Wed, 9 Jan 2008 16:41:43 +0100 X-Mailer: Apple Mail (2.753) X-Miltered: at concorde with ID 4784EB32.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; jfla:01 jfla:01 coq:01 semantiques:01 coq:01 renaud:01 semantiques:01 renaud:01 dejeuner:01 invitee:01 weis:01 theoreme:01 formelle:01 algorithme:01 d'allocation:01 2e appel a participation JOURNEES FRANCOPHONES DES LANGAGES APPLICATIFS INRIA 26 au 29 janvier 2008 Etretat, France http://jfla.inria.fr/2008 Le programme des 19=E8mes JFLA est maintenant =E9tabli; vous trouverez aupr=E8s du site des journ=E9es http://jfla.inria.fr/2008 tout renseignement n=E9cessaire =E0 votre inscription. Merci de vous inscrire avant le *** 15 janvier 2008 ***. Bien cordialement, Sandrine Blazy ************************************************************************=20= ******** Programme Premier jour: 26 janvier 2008 * 15h - 15h30 Accueil - Pr=E9sentation * 15h30 - 17h Cours Coq par Yves Bertot: S=E9mantiques en Coq * 17h - 17h30 Pause-caf=E9 * 17h30 - 19h Cours Focal par Renaud Rioboo: Concevoir et organiser une librairie de math=E9matiques =20 effectives * 19h00 D=EEner Deuxi=E8me jour: 27 janvier 2008 * 9h - 10h30 Cours Coq par Yves Bertot: S=E9mantiques en Coq * 10h30 - 11h Pause-caf=E9 * 11h30 - 12h30 Cours Focal par Renaud Rioboo: Concevoir et organiser une librairie de math=E9matiques =20 effectives * 12h30 - 14h D=E9jeuner * 14h00 - 18h Excursion: une balade =E0 pied * 19h00 D=EEner Troisi=E8me jour: 28 janvier 2008 * 9h00 - 10h00 Conf=E9rence invit=E9e Les types =E0 relations. Pierre Weis (INRIA). * 10h - 10h30 Pause-caf=E9 * 10h30 - 11h Formalisation des math=E9matiques: une preuve du =20 th=E9or=E8me de Cayley-Hamilton. Sidi Ould Biha. * 11h - 11h30 A formal verification for Kantorovitch's theorem. Ioana Pasca. * 11h30 - 12h00 V=E9rification formelle d'un algorithme =20 d'allocation de registres par coloration de graphes. Sandrine Blazy, Beno=EEt Robillard et =C9ric Soutif. * 12h00 - 14h D=E9jeuner * 14h00 - 14h30 De la webradio lambda =E0 la lambda-webradio. David Baelde et Samuel Mirman. * 14h30 - 15h Le caract=E8re ' =E0 la rescousse. Boris Yakobowski. * 15h00 - 15h30 Types simples, logique et coercions implicites. Cody Roux. * 15h30 - 16h Pause caf=E9 * 16h - 16h30 SAT-Micro : petit mais costaud !. Sylvain Conchon, Johannes Kanig et St=E9phane Lescuyer. * 16h30 - 17h V=E9rification formelle du tri par tas - =C9tude =20 op=E9rationnelle. Pascal Manoury. * 17h - 17h30 M=E9taprogrammation fonctionnelle appliqu=E9e =E0 la =20= g=E9n=E9ration d'un DSL d=E9di=E9 =E0 la programmation parall=E8le. Jocelyn S=E9rot et Jo=EBl Falcou. * 19h00 D=EEner Quatri=E8me jour: 29 janvier 2008 * 9h00 - 10h00 Conf=E9rence invit=E9e Impl=E9mentations s=FBres de sessions typ=E9es. C=E9dric Fournet (Microsoft Research). * 10h - 10h30 Pause-caf=E9 * 10h30 - 11h00 Une axiomatique de la g=E9om=E9trie plane en Coq. Jean Duprat. * 11h00 - 11h30 Gagner en passant =E0 la corde. Jean-Christophe Filli=E2tre. * 11h30 - 11h45 Bilan et cl=F4ture des Journ=E9es * 11h45 - 12h30 D=E9jeuner Pour tout renseignement, contacter Ga=EBlle Dorkeld INRIA Rocquencourt Bureau des Cours et Colloques (JFLA2008) Domaine de Voluceau - BP 105 78153 Le Chesnay Cedex T=E9l.: +33 (0) 1 39 63 56 00 - Fax : +33 (0) 1 39 63 56 38 email : Gaelle.Dorkeld@inria.fr http://jfla.inria.fr/2008/