Les vingt-septièmes Journées Francophones des Langages Applicatifs se tiendront au Grand Hôtel des Thermes de Saint-Malo, en Bretagne.

Les JFLA réunissent concepteurs, utilisateurs et théoriciens ; elles ont pour ambition de couvrir les domaines des langages applicatifs, de la preuve formelle, de la vérification de programmes, et des objets mathématiques qui sous-tendent ces outils. Ces domaines doivent être pris au sens large : nous souhaitons promouvoir les ponts entre les différentes thématiques.

  • Langages fonctionnels et applicatifs: sémantique, compilation, optimisation, typage, mesures, extensions par d'autres paradigmes.
  • Assistants de preuve: implémentation, nouvelles tactiques, développements présentant un intérêt technique ou méthodologique.
  • Logique, correspondance de Curry-Howard, réalisabilité, extraction de programmes, modèles.
  • Spécification, prototypage, développements formels d'algorithmes.
  • Vérification de programmes ou de modèles, méthode déductive, interprétation abstraite, raffinement.
  • Utilisation industrielle des langages fonctionnels et applicatifs, ou des méthodes issues des preuves formelles, outils pour le web.

Dates

  • 23 octobre 28 octobre 2015 : soumission des résumés
  • 30 octobre 6 novembre 2015 : soumission des articles
  • 4 décembre 2015 : notification aux auteurs
  • 18 décembre 2015 : remise des articles définitifs
  • 8 janvier 17 janvier 2016 : clôture des inscriptions
  • 27 au 30 janvier 2016 : journées

Appel à communication

Nous acceptons deux types de soumissions :

  • Article de recherche de quinze pages au plus, portant sur des travaux originaux. Nous accepterons volontiers des travaux en cours (pour lesquels l'aspect recherche n'est pas entièrement terminé) tout particulièrement s'il s'agit de jeunes chercheurs. Dans tous les cas, la forme de l'article devra être soignée. Les articles sélectionnés seront publiés dans les actes de la conférence, les auteurs seront invités à faire une présentation en vingt-cinq minutes lors des journées.
  • Exposé court pour décrire un prototype, faire la démonstration d'un outil, reparler d'un article déjà publié, rechercher de l'aide pour résoudre un problème particulier. Dans ce cas, nous vous demandons seulement de soumettre un résumé de deux à trois pages, qui nous permettra de sélectionner les orateurs en cas de forte affluence.

Les articles soumis aux JFLA sont relus par au moins deux personnes s'ils sont acceptés, trois personnes s'ils sont rejetés. Les critiques des relecteurs sont toujours bienveillantes et la plupart du temps encourageantes et constructives, même en cas de rejet.

Il n'y a donc pas de raison de ne pas soumettre aux JFLA !

Soumissions

Les soumissions peuvent être rédigées en français ou en anglais, mais elles sont limitées à 15 pages LaTeX dans le style des actes.

La soumission finale doit être une archive tar compressée de nom idx_nom.tgzidx est le numéro de soumission et nom est le nom du premier auteur de l'article. L'archive doit contenir la version finale au format PDF, ainsi que tout le matériel nécessaire à sa génération.

Cette soumission est à envoyer par courier électronique au vice-président avant le 18 décembre 2015.

Comité de programme

Jade Alglave Microsoft Research Cambridge et
University College London (présidente)
Julien Signoles CEA LIST (vice-président)
Thibaut Balabonski LRI, Université Paris-Sud
Thomas Braibant Jane Street
Sylvie Boldo Inria, LRI
Cyril Cohen Inria Sophia Antipolis - Méditerranée
Claire David Université Paris-Est Marne-la-Vallée
Cezara Dragoi Inria Paris-Rocquencourt
Jean-Marie Madiot Princeton University
Gustavo Petri LIAFA - Université Paris Diderot (Paris 7)
Boris Yakobowski CEA LIST

Appel à participation

Inscrivez-vous aux journées jusqu'au dimanche 17 janvier. L'inscription est un forfait qui comprend l'hébergement et la restauration sur le site des journées:

  • 650€ TTC en chambre simple;
  • 490€ TTC en chambre double.

Infos pratiques

Pour venir aux journées, vous pouvez venir en train par la gare de Saint-Malo. Une navette permettra d'atteindre facilement l'hôtel.

  • Gare - hôtel : mercredi 27 janvier, en liaison avec le train de Paris et Rennes arrivant à 14h32;
  • Hôtel - gare : samedi 30 janvier, en liaison avec le train pour Paris partant à 12h15.

Attention: pour cause de travaux sur les voies, il n'y a aucun train (autre que le TGV indiqué) entre Rennes et Paris du samedi midi au dimanche midi.

Programme

Deux cours et deux exposés invités sont prévus.

Cours invités

  • Pierre-Yves Strub (IMDEA Software Institute).
    Une introduction à la preuve de sécurité formelle avec le système EasyCrypt.
  • Nobuko Yoshida (Imperial College London).
    Session types and their applications.

Exposés invités

  • Patrick Cousot (New York University).
    Construction of invariance proof methods.
  • Jonathan Protzenko (Microsoft Research).
    The global sequence protocol: a memory model for distributed systems

Articles acceptés

9 articles de recherche et 3 exposés courts ont été acceptés. Le programme des journées est maintenant disponible.
  • S. Archipoff et D. Janin. Pour un raffinement spatio-temporel tuilé.
  • P.-L. Bégay, P. Manoury et I. Rakotonirina. Une mesure ordinale pour les preuves de terminaison en Coq.
  • M. Bodin, T. Jensen and A. Schmitt. An Abstract Separation Logic for Interlinked Extensible Records.
  • B. Canou, Ç. Bozman et G. Henry. Sous le capot du MOOC OCaml.
  • S. Castellan. Weak memory models using event structures.
  • R. El Sibaïe et E. Chailloux. Pendulum : une extension réactive pour la programmation Web en OCaml.
  • J.-C. Filliâtre et M. Pereira. Itérer avec confiance.
  • C. Gries, P. Boutry et J. Narboux. Somme des angles d'un triangle et unicité de la parallèle : une preuve d'équivalence formalisée en Coq.
  • F. Pottier. Reachability and error diagnosis in LR(1) automata.
  • A.-G. Bosser, P. Courtieu, J. Forest et M.-V. Aponte. Une preuve est une histoire (présentation courte).
  • J.-C. Lechenet, N. Kosmatov. et P. Le Gall. Coq a dit : fromage tranché ne peut cacher ses trous (présentation courte).
  • B. Rognier et G. Duhamel. Présentation de la plateforme edukera (présentation courte).

Soutiens

Les JFLA 2016 sont organisés en collaboration avec Inria et bénéficient des soutiens financiers du CEA LIST, du GDR GPL, d'OcamlPro, de Microsoft Research, de Jane Street et de TrustInSoft.

   

 

Contact

Pour tout renseignement, contacter le vice-président.