JFLA 2017

Gourette
mercredi 4 janvier 2017

samedi 7 janvier 2017

Dates importantes

Soumission des résumés 2 octobre 2016 25 septembre 2016
Soumission des articles 18 octobre 2016 16 octobre 2016 9 octobre 2016
Notification aux auteurs 18 novembre 2016
Soumission version finale 27 novembre 2016
Clôture des inscriptions 11 décembre 2016

Programme

Cours invités

Guillaume Burel (ENSIIE)
Exprimer ses théories en Dedukti, le vérificateur de preuves universel
Benjamin Canou (OCamlPro SAS)
Comment programmer en OCaml aujourd'hui

Exposés invités

Damien Doligez (Inria Paris)
Zenon
Stéphane Lescuyer et Florence Plateau (Prove & Run)
Langage et outil pour la preuve d'un micro-noyau

En détails

mercredi 4 janvier

  • 18:10 — 19:40
    Benjamin Canou (OCamlPro SAS)
    Comment programmer en OCaml aujourd'hui

jeudi 5 janvier

  • 09:00 — 10:00
    Stéphane Lescuyer et Florence Plateau (Prove & Run)
    Langage et outil pour la preuve d'un micro-noyau
  • 10:00 — 10:30
    R. Rieu-Helft et P. Cuoq
    Result graphs for an abstract interpretation-based static analyzer
  • 11:20 — 11:50
    G. Baudart , L. Mandel , O. Tardieu et M. Vaziri
    CloudLens: un langage de scripts pour l'analyse de données semi-structurées
  • 11:20 — 11:50
    S. Varoumas , E. Chailloux et B. Vaugon
    OCaLustre : une extension synchrone d'OCaml pour la programmation de microcontrôleurs
  • 11:50 — 12:20
    N. Jeannerod
    Le coquillage dans le CoLis-mateur: Formalisation d'un langage de programmation de type shell
  • 16:40 — 17:10
    R. Bonichon (CEA LIST) et P. Weis (Inria Paris)
    Format Unraveled
  • 17:10 — 17:30
    D. Ly et J. Garrigue
    Des unités dans le typeur
  • 17:30 — 17:50
    M. Clochart
    Preuves taillées en biseau
  • 18:10 — 19:40
    Benjamin Canou (OCamlPro SAS)
    Comment programmer en OCaml aujourd'hui

vendredi 6 janvier

  • 09:00 — 10:00
    Damien Doligez (Inria Paris)
    Zenon
  • 10:00 — 10:30
    J. Auerbach , M. Hirzel , L. Mandel , A. Shinnar et J. Siméon
    Prototyper un compilateur de requêtes avec Coq
  • 10:50 — 11:20
    M. Puech
    Typeful Continuations
  • 11:20 — 11:50
    S. Boulier , P.-M. Pédrot et N. Tabareau
    Modèles de la théorie des types donnés par traduction de programmes
  • 11:50 — 12:20
    G. Cabon et A. Schmitt
    Non-Interfererence through Annotated Multisemantics
  • 16:40 — 17:10
    T. Bourke , P.-É. Dagand , M. Pouzet et L. Rieg
    Vérification de la génération modulaire du code impératif pour Lustre
  • 17:10 — 17:30
    D. Janin et B. Serpette
    Causalité dans les calculs d'événements
  • 17:30 — 17:50
    C. Cohen et D. Rouhling
    A refinement-based approach to large scale reflection for algebra
  • 18:10 — 19:40
    Guillaume Burel (ENSIIE)
    Exprimer ses théories en Dedukti, le vérificateur de preuves universel

samedi 7 janvier

  • 09:00 — 09:30
    M. Pereira (LRI)
    Défonctionnaliser pour prouver
  • 09:30 — 10:00
    R. Chen et J.-J. Lévy
    Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe
  • 10:20 — 11:50
    Guillaume Burel (ENSIIE)
    Exprimer ses théories en Dedukti, le vérificateur de preuves universel

Appel à soumission

 Les 28es Journées Francophones des Langages Applicatifs (JFLA) se tiendront à Gourette, plus précisément Belambra Club , du mercredi 4 janvier 2017 au samedi 7 janvier 2017 .

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.

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 !

Soumission

Nous acceptons deux types de soumissions :

  • Article de recherche de seize pages au plus (bibliographie incluse), portant sur des travaux originaux. Nous acceptons des travaux en cours, pour lesquels l'aspect recherche n'est pas entièrement finalisé.
  • Article court de huit pages au plus (bibliographie incluse), pour décrire un prototype, faire la démonstration d'un outil, rechercher de l'aide pour résoudre un problème particulier, ou reparler d'un papier déjà publié.

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, et les auteurs seront invités à faire une présentation lors des journées, de vingt-cinq minutes pour les articles longs et de quinze minutes pour les courts.

L'article peut être rédigé en anglais, auquel cas la présentation devra être effectuée en français. Néanmoins, dans le cas où il s'agit d'une republication au format court d'un article déjà publié, la publication doit être en français et la publication originale en anglais.

Organisation

Comité de programme

Julien Signoles CEA LIST Président
Sylvie Boldo Inria Saclay-Île de France, LRI Vice-présidente
June Andronick Data61/CSIRO & UNSW
Anne-Gwenn Bosser ENIB, Lab-STICC
Thomas Gazagnaire Docker
Mohamed Iguernlala OCamlPro SAS
Frédéric Loulergue SICCS, Northern Arizona University
Laurent Mounier Verimag, Université Grenoble Alpes
François Pottier Inria Paris
Sylvain Salvati Université Lille 1
Mihaela Sighireanu Université Paris 7
Francesco Zappa Nardelli Inria Paris

Soutiens

Cette édition des JFLA bénéficie du soutien financier des partenaires ci-dessous. Merci à eux !