The Coq mailing list

[David Baelde <david.baelde AT gmail.com>]

   *** Appel à participation, merci de diffuser largement ***


            JFLA'2015 (http://jfla.inria.fr/2015/)

        Journées Francophones des Langages Applicatifs

        au Val d'Ajol, du 7 janvier au 10 janvier 2015


Les incriptions aux JFLAs sont désormais ouvertes. Vous trouverez
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
-----------------

25 novembre 2015 : date limite d'inscription aux journées

7 au 10 janvier 2015 : journées

Soutien Financier
-----------------

Grâce au soutien des GDR GPL et IM, nous avons la possibilité
de financer une partie des journées pour quelques étudiants
ou jeunes chercheurs. Si vous souhaitez demander ce soutien,
contactez David Baelde au plus tôt et avant le 16 novembre.

Cours et exposés invités
------------------------

. Stephan Merz (Inria Nancy & LORIA) :
    Vérification d'algorithmes distribués
. Manuel Serrano (Inria Sophia-Antipolis) : Programmation web en Hop

. Alastair Donaldson (Imperial College London) :
    Verification techniques for GPU kernels
. Marco Gaboardi (University of Dundee) : Differential privacy

Articles acceptés (par ordre de soumission)
-------------------------------------------

Arvid Jakobsson, Nikolai Kosmatov and Julien Signoles.
Rester statique pour devenir plus rapide, plus précis et plus mince

Francois Pottier.
Depth-First Search and Strong Connectivity in Coq

Alix Trieu, Robert Dockins and Andrew Tolmach.
Static conflict detection for a policy language

Simon Castellan.
La stratégie de la fourchette

Jérôme Fortier. Higher-Order Trees are Circularly Computable

Steven De Oliveira, Virgile Prevosto and Sébastien Bardin.
Au temps en emporte le C

Martin Clochard and Léon Gondelman.
Double WP: vers une preuve automatique d'un compilateur

Martin Escarrá, Petar Maksimović and Alan Schmitt. HOCore in Coq

Théis Bazin and David Janin.
Flux média tuilés polymorphes :
une sémantique opérationnelle en Haskell

David Braun and Nicolas Magaud.
Des preuves formelles en Coq du théorème de Thalès pour les cercles

Çagdas Bozman, Grégoire Henry, Fabrice Le Fessant,
Michel Mauny and Mohamed Iguernelala.
ocp-memprof: un profileur mémoire pour OCaml

Richard Genestier, Alain Giorgetti and Guillaume Petiot.
Gagnez sur tous les tableaux

Benjamin Farinier, Thomas Gazagnaire and Anil Madhavapeddy.
Mergeable persistent data-structures

Paul Brunet and Damien Pous.
Decidability of Identity-free Relational Kleene Lattices

Gabriel Scherer. Normalization by realizability also evaluates

Catherine Dubois, Sourour Elloumi, Benoit Robillard and Clément Vincent.
Graphes et couplages maximaux en Coq

Alexandre Maréchal and Michaël Périn.
A linearization technique for multivariate polynomials using
convex polyhedra based on Handelman's theorem

Comité de programme
-------------------

David Baelde           LSV, ENS Cachan (Président)
Jade Alglave           UCL (Vice-présidente)
Maria-Virginia Aponte  CNAM
Sylvie Boldo           Inria, LRI
Pierre Clairambault    ENS Lyon
Delphine Demange       IRISA, Université de Rennes 1
Kim Nguyen             LRI, Université Paris-Sud 11
Florence Plateau       Prove & Run
Christophe Raffalli    LAMA, Université de Savoie
Julien Signoles        CEA LIST
Pierre-Yves Strub      IMDEA Software Institute
Jules Villard          Imperial College London

Pour tout renseignement, contacter
  David Baelde 
<baelde AT lsv.ens-cachan.fr>