JFLA 2024

Journées Francophones des Langages Applicatifs
Saint-Jacut-de-la-Mer
mardi 30 janvier 2024
vendredi 2 février 2024
Abbaye de Saint-Jacut
L'Abbaye de Saint-Jacut en hiver

Actes

Les actes des JFLA 2024 sont disponibles sur HAL. Ils sont téléchargeables depuis le lien ci-dessous.

Les articles sont aussi disponibles, un à un, depuis les liens indiqués dans le programme détaillé.

Dates importantes

Attention, ces dates sont fermes et définitives.
Il n’y aura pas d’extension.
Les dates échoient à la fin du jour, AoE.

Soumission des résumés 19 octobre 2023
Soumission des articles 19 octobre 2023
Notification aux auteurs 1er décembre 2023
Envoi des versions finales 18 décembre 2023
Inscriptions 2 décembre 2023 - 8 janvier 2024
Conférence 30 janvier 2024 - 2 février 2024

Inscription

Type d'inscription Montant T.T.C.
Tarif de base 650 €
Étudiant·e orateur·ice pour un article accepté (stagiaire, personne inscrite en thèse) 0 €
Inscription subventionnée (voir conditions spécifiques) 0 €


Les exposés scientifiques commencent le mardi 30 janvier au matin. Il est donc conseillé d’arriver sur place le lundi 29 janvier au soir. Les journées se terminent le vendredi 2 février, juste après le déjeuner.

Ces frais couvrent l’aller-retour en autocar entre Rennes et l’Abbaye de Saint-Jacut (voir ci-dessous), le logement en chambre individuelle du lundi 29 janvier au vendredi 02 février (4 nuits, avec petit-déjeuner), les repas, les collations, l’activité en plein air, et la participation à tous les exposés.

Grâce à nos généreux soutiens, l’inscription est gratuite pour :

  • les étudiant·es orateur·ices dont l'article a été accepté,
  • et quelques participants qui obtiendront une subvention après examen de leur demande, et dans la limite des fonds disponibles.

L’Agence VERT COM gère le processus d’inscription et de règlement des frais aux JFLA 2024.

Pour plus d’informations (modalités de paiement, conditions d’annulation, etc), consultez les Conditions Générales de Ventes.

Pour toute question concernant les inscriptions, contactez le comité d’organisation à l’adresse jfla24-inscriptions@inria.fr.


Conditions spécifiques : inscriptions subventionnées [Cliquer pour (dé)plier]

Les JFLA 2024 proposent un petit nombre d'inscriptions subventionnées pour les personnes souhaitant assister (orateur.ice ou non) aux journées et qui ne disposent pas des ressources financières suffisantes dans le cadre de leurs activités professionnelles (poste permanent ou non) ou à visée professionelle (recherche de poste, en cours de formation, etc).

La subvention est individuelle. Elle couvre entièrement les frais d'inscription au tarif de base (soit 650 euros). Les autres frais liés au déplacement (transport, frais annexes durant le trajet, mission) ne sont pas couverts par cette subvention.

Pour candidater, envoyez par courriel au comité d'organisation les informations suivantes :

  • vos nom et prénom,
  • votre statut actuel et votre affiliation éventuelle,
  • votre ville de résidence principale,
  • vos motivations personnelles pour la demande de subvention.
Toutes les informations fournies nous permettront de réaliser les arbitrages nécessaires.

Les candidatures sont recevables jusqu’au vendredi 29 décembre 2023.
Les notifications de subvention (accord ou refus) seront communiquées individuellement au plus tard le jeudi 04 janvier 2024.

Le processus de sélection est entièrement bénévole et les fonds disponibles sont limités. Nous comptons sur vous pour ne solliciter une subvention qu'en cas de besoin réel.


Navettes en autocar Rennes - Abbaye de Saint-Jacut [Cliquer pour (dé)plier]

Pour rejoindre et quitter le site facilement, une navette est prévue pour les participants à l'aller et au retour.
La liaison sera établie entre la gare routière de Rennes et l’Abbaye de Saint-Jacut-de-la-Mer en autocar (1h30 de trajet).

  • Aller : lundi 29 janvier (Gare routière de Rennes - Abbaye de Saint-Jacut), départ à 17h30.
  • Retour : vendredi 2 février (Abbaye de Saint-Jacut - Gare routière de Rennes), départ avant 13h30 pour une arrivée à 15h00.


Activité de plein air mercredi après-midi [Cliquer pour (dé)plier]

Nous vous proposons une randonnée pédestre commentée de la Pointe du Chevet (durée 2h30).
La randonnée accompagnée est tout public et accessible à presque tous (accès PMR non garanti).
Elle se déroule en grande partie sur le GR34.

Pensez à prévoir :

  • une tenue adaptée à la marche
  • de bonnes chaussures
  • un coupe-vent et/ou un vêtement de pluie

Les participants qui le souhaitent pourront bien sûr rester dans l'enceinte de l'Abbaye, et utiliser les salles mises à notre disposition.

Programme

Exposés invités

Guillaume Baudart (Université Paris Cité, Inria) et Christine Tasson (ISAE-SUPAERO)
Programmation réactive probabiliste [article] [présentation]

Le résumé étendu de l’exposé est accessible ici. Les deux supports de présentation et la démonstration de Mini ProbZelus sont disponibles dans l’archive .zip de la présentation.

Micaela Mayero (LIPN, Université Sorbonne Paris Nord) et Pierre Rousselin (LAGA, Université Sorbonne Paris Nord)
Utilisation de Coq pour l'enseignement en Licence 1 et en Seconde [article] [présentation]

Nous avons créé en septembre 2021 un cours récurrent de 18h d’« Initiation aux preuves formelles » avec Coq au premier semestre de L1 double-licence mathématiques et informatique à l’université Sorbonne Paris Nord. Une expérience ponctuelle de 9h a également eu lieu en 2022 avec des élèves de seconde du lycée Joséphine Baker de Pierrefitte sur-Seine.

Cet exposé est un retour sur ces expériences. Nous présenterons en détail certaines séances de travaux pratiques données en L1, la méthode employée pour l’écriture des sujets, l’évolution de ce module ainsi que les difficultés rencontrées par les enseignant•e•s et les étudiant•e•s. Enfin, nous évoquerons des pistes d’évolution pour l’enseignement des mathématiques avec Coq au niveau L1.

Des temps d’échange et d’expérimentation sont prévus. Les participants qui ne connaissent pas Coq pourront se servir des sujets de travaux pratiques comme d’un tutoriel ; les experts de Coq se tourneront d’avantage vers des questions pédagogiques et techniques.

Matthieu Sozeau (Inria)
MetaCoq - towards a certified kernel and extraction for Coq [article] [présentation] [URL]

MetaCoq est une librairie qui a pour but d’étudier la théorie et l’implémentation de Coq lui-même, en Coq. MetaCoq comprend quatre composants principaux. Le premier, nommé Template-Coq, est une réification en Coq des termes et environnements manipulés par le noyau de Coq (en OCaml), qui permet d’interopérer directement avec le système en développant des métaprogrammes à l’aide du langage Gallina et d’une monade représentant l’interface du noyau de Coq. Le second, PCUIC, est une formalisation d’une variante du système de types du calcul de constructions inductives et de ses propriétés métathéoriques essentielles, qui permet de garantir la correction du système et d’étudier ses extensions possibles. Le troisième composant est une version certifiée d’un vérificateur de types et d’environnements pour ce calcul, garantissant la décidabilité de l’inférence de types et sa correction et complétude vis-à-vis de la spécification de PCUIC. Enfin, le quatrième composant est un développement certifié de la procédure d’effacement des preuves et des types de PCUIC vers un lambda-calcul pur, qui forme le coeur du mécanisme d’extraction de Coq, permettant en particulier d’extraire le vérificateur de types vers des langages exécutables de façon sûre. Au cours de cet exposé, je présenterai un tour d’horizon de ces quatre composants et leur utilisation pour la production de programmes certifiés en Coq avec des garanties de sûreté maximales.

Jules Villard (Meta)
Infer: a compositional and extensible platform for static analysis [article]

Infer is an open-source static analysis platform that is used to prevent classes of bugs in code at Meta. Every month, Infer runs on thousands of code changes and detects thousands of bugs that are fixed by developers before they reach production. Over the years, Infer has evolved from a standalone analyser based on Separation Logic to a powerful platform for implementing cross-language interprocedural analyses. Static analysis writers only need to provide an intraprocedural analysis that computes the summary for a single procedure and Infer will transform it into a compositional interprocedural analysis that scales to millions of lines of real code.

In this talk, we’ll go through some of the formal methods from program verification that are implemented inside Infer such as separation logic, abstract interpretation, and incorrectness logic, and how they make it a valuable tool for programmers.


Programme détaillé

lundi 29 janvier

mardi 30 janvier

  • 09:00 — 09:10
    Delphine Demange et Adrien Guatto
    Ouverture des JFLA 2024
  • 09:10 — 10:10
    Micaela Mayero (LIPN, Université Sorbonne Paris Nord) et Pierre Rousselin (LAGA, Université Sorbonne Paris Nord)
    Utilisation de Coq pour l'enseignement en Licence 1 et en Seconde [article] [présentation]

    Nous avons créé en septembre 2021 un cours récurrent de 18h d’« Initiation aux preuves formelles » avec Coq au premier semestre de L1 double-licence mathématiques et informatique à l’université Sorbonne Paris Nord. Une expérience ponctuelle de 9h a également eu lieu en 2022 avec des élèves de seconde du lycée Joséphine Baker de Pierrefitte sur-Seine.

    Cet exposé est un retour sur ces expériences. Nous présenterons en détail certaines séances de travaux pratiques données en L1, la méthode employée pour l’écriture des sujets, l’évolution de ce module ainsi que les difficultés rencontrées par les enseignant•e•s et les étudiant•e•s. Enfin, nous évoquerons des pistes d’évolution pour l’enseignement des mathématiques avec Coq au niveau L1.

    Des temps d’échange et d’expérimentation sont prévus. Les participants qui ne connaissent pas Coq pourront se servir des sujets de travaux pratiques comme d’un tutoriel ; les experts de Coq se tourneront d’avantage vers des questions pédagogiques et techniques.

  • 10:10 — 10:30
    Reynald Affeldt et Zachary Stone
    Towards the Fundamental Theorem of Calculus for the Lebesgue integral in Coq [article] [présentation]
  • 11:00 — 11:30
    Claude Marché et Denis Cousineau
    De l'avantage de nuancer les décisions binaires [article] [présentation]
  • 11:30 — 11:50
    Maximiliano Cristiá et Catherine Dubois
    Comparing EventB, {log} and Why3 models of Sparse Sets [article] [présentation]
  • 11:50 — 12:10
    Ambroise Lafont
    A diagram editor to mechanise categorical proofs [article] [présentation]
  • 14:00 — 15:30
    Jules Villard (Meta)
    Infer: a compositional and extensible platform for static analysis [article]

    Infer is an open-source static analysis platform that is used to prevent classes of bugs in code at Meta. Every month, Infer runs on thousands of code changes and detects thousands of bugs that are fixed by developers before they reach production. Over the years, Infer has evolved from a standalone analyser based on Separation Logic to a powerful platform for implementing cross-language interprocedural analyses. Static analysis writers only need to provide an intraprocedural analysis that computes the summary for a single procedure and Infer will transform it into a compositional interprocedural analysis that scales to millions of lines of real code.

    In this talk, we’ll go through some of the formal methods from program verification that are implemented inside Infer such as separation logic, abstract interpretation, and incorrectness logic, and how they make it a valuable tool for programmers.

  • 16:00 — 16:30
    Mamy Razafintsialonina , David Bühler , Antoine Miné , Valentin Perrelle et Julien Signoles
    Réutilisations de caches et d'invariants pour l'analyse statique incrémentale [article]
  • 16:30 — 17:00
    Tristan Le Gall , Jan Rochel , Florian Faissole , Julien Signoles et Denis Cousineau
    Alias : pointeurs espionnés en série [article] [présentation]
  • 17:00 — 17:20
    Arthur Correnson
    À la recherche de tous les vrais bugs - Vérification formelle d'un détecteur de bugs automatique [article]
  • 17:20 — 17:50
    Clément Allain et Gabriel Scherer
    Correct tout seul, sûr à plusieurs [article] [présentation]
  • 17:50 — 18:05
    Présentation OCamlPro [présentation] [URL]

mercredi 31 janvier

  • 09:00 — 10:00
    Micaela Mayero (LIPN, Université Sorbonne Paris Nord) et Pierre Rousselin (LAGA, Université Sorbonne Paris Nord)
    Utilisation de Coq pour l'enseignement en Licence 1 et en Seconde [article] [présentation]

    Nous avons créé en septembre 2021 un cours récurrent de 18h d’« Initiation aux preuves formelles » avec Coq au premier semestre de L1 double-licence mathématiques et informatique à l’université Sorbonne Paris Nord. Une expérience ponctuelle de 9h a également eu lieu en 2022 avec des élèves de seconde du lycée Joséphine Baker de Pierrefitte sur-Seine.

    Cet exposé est un retour sur ces expériences. Nous présenterons en détail certaines séances de travaux pratiques données en L1, la méthode employée pour l’écriture des sujets, l’évolution de ce module ainsi que les difficultés rencontrées par les enseignant•e•s et les étudiant•e•s. Enfin, nous évoquerons des pistes d’évolution pour l’enseignement des mathématiques avec Coq au niveau L1.

    Des temps d’échange et d’expérimentation sont prévus. Les participants qui ne connaissent pas Coq pourront se servir des sujets de travaux pratiques comme d’un tutoriel ; les experts de Coq se tourneront d’avantage vers des questions pédagogiques et techniques.

  • 10:00 — 10:15
    Annonces du GDR GPL (Génie de la Programmation et du Logiciel) [présentation] [URL]
  • 10:45 — 12:15
    Matthieu Sozeau (Inria)
    MetaCoq - towards a certified kernel and extraction for Coq [article] [présentation] [URL]

    MetaCoq est une librairie qui a pour but d’étudier la théorie et l’implémentation de Coq lui-même, en Coq. MetaCoq comprend quatre composants principaux. Le premier, nommé Template-Coq, est une réification en Coq des termes et environnements manipulés par le noyau de Coq (en OCaml), qui permet d’interopérer directement avec le système en développant des métaprogrammes à l’aide du langage Gallina et d’une monade représentant l’interface du noyau de Coq. Le second, PCUIC, est une formalisation d’une variante du système de types du calcul de constructions inductives et de ses propriétés métathéoriques essentielles, qui permet de garantir la correction du système et d’étudier ses extensions possibles. Le troisième composant est une version certifiée d’un vérificateur de types et d’environnements pour ce calcul, garantissant la décidabilité de l’inférence de types et sa correction et complétude vis-à-vis de la spécification de PCUIC. Enfin, le quatrième composant est un développement certifié de la procédure d’effacement des preuves et des types de PCUIC vers un lambda-calcul pur, qui forme le coeur du mécanisme d’extraction de Coq, permettant en particulier d’extraire le vérificateur de types vers des langages exécutables de façon sûre. Au cours de cet exposé, je présenterai un tour d’horizon de ces quatre composants et leur utilisation pour la production de programmes certifiés en Coq avec des garanties de sûreté maximales.

jeudi 1er février

  • 09:00 — 10:00
    Guillaume Baudart (Université Paris Cité, Inria) et Christine Tasson (ISAE-SUPAERO)
    Programmation réactive probabiliste [article] [présentation]

    Le résumé étendu de l’exposé est accessible ici. Les deux supports de présentation et la démonstration de Mini ProbZelus sont disponibles dans l’archive .zip de la présentation.

  • 10:30 — 10:45
    Milla Valnet , Nathanaëlle Courant , Guillaume Bury , Pierre Chambart et Vincent Laviron
    Chamelon : un minimiseur de programmes pour et en OCaml [article] [présentation]
  • 10:50 — 11:20
    François Pottier
    Correct, fast LR(1) unparsing [article] [présentation]
  • 11:20 — 11:40
    Guillaume Bertholon , Arthur Charguéraud et Thomas Koehler
    Source-to-source optimizations validated using Separation Logic [article]
  • 11:40 — 12:00
    David Monniaux et Sylvain Boulmé
    Chamois: agile development of CompCert extensions for optimization and security [article] [présentation]
  • 12:00 — 12:20
    Frédéric Recoules et Sébastien Bardin
    L'interprète, le JIT et la licorne [article] [présentation]
  • 14:00 — 14:30
    Lison Blondeau-Patissier
    Resource categories from differential categories [article] [présentation]
  • 14:30 — 15:00
    Martin Andrieux et Alan Schmitt
    Skeletal semantics of a fragment of Python [article] [présentation]
  • 15:00 — 15:30
    Colin Riba et Solal Stern
    Liveness properties in Geometric Logic for domain-theoretic streams [article]
  • 15:30 — 15:50
    Hadrien Renaud
    Executable semantics of Arm's Architecture Specification Language [article] [présentation]
  • 15:50 — 16:10
    Sydney Congard
    Towards a linear functional translation for borrowing [article] [présentation]
  • 16:40 — 17:00
    Mickaël Laurent
    Type inference of polymorphic and overloaded functions - Towards static typing of dynamic languages [article]
  • 17:00 — 17:20
    Bertrand Jeannet , Étienne Closse , Fabien Gaucher et Daniel Weil
    Stimulus : un langage synchrone à contraintes [article]
  • 17:20 — 17:40
    Guillaume Duboc
    Un prototype de système de types graduels ensemblistes pour Elixir [article]
  • 17:40 — 18:10
    Thomas Bagrel
    Destination-passing style programming: a Haskell implementation [article]
  • 18:10 — 18:30
    Jean Caspar et Guillaume Munch-Maccagnoni
    Modular efficient deconstruction with typed pointer reversal [article]

vendredi 2 février

  • 09:00 — 10:00
    Guillaume Baudart (Université Paris Cité, Inria) et Christine Tasson (ISAE-SUPAERO)
    Programmation réactive probabiliste [article] [présentation]

    Le résumé étendu de l’exposé est accessible ici. Les deux supports de présentation et la démonstration de Mini ProbZelus sont disponibles dans l’archive .zip de la présentation.

  • 10:30 — 11:00
    Loïc Correnson
    Packaging proofs with Why3find [article] [présentation]
  • 11:00 — 11:20
    Louise Dubois de Prisque
    Décision automatique de relations inductives pour SMTCoq (JFLA 2023) [article] [présentation]
  • 11:20 — 11:40
    Pierre-Évariste Dagand , Pierre Letouzey et Ellenor Fatemeh Taghayor
    Rough Pearl: manufacturing Cons-cells [article]
  • 11:40 — 11:45
    Adrien Guatto et Delphine Demange
    Clôture des JFLA 2024

Appel à soumission

Les 35es Journées Francophones des Langages Applicatifs (JFLA) se tiendront à Saint-Jacut-de-la-Mer, plus précisément à l' Abbaye de Saint-Jacut , du mardi 30 janvier 2024 au vendredi 2 février 2024 .

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 théorique, 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, vérification déductive, interprétation abstraite, raffinement.
  • Utilisation industrielle des langages fonctionnels et applicatifs, ou des méthodes issues de la communauté scientifique. Outils et plateformes pour le web.
  • Problématiques d'enseignement, de formation, ou de diffusion des langages fonctionnels et applicatifs. Environnements et méthodologies de développement, retours d'expérience.

Les articles soumis aux JFLA sont relus par au moins deux personnes s'ils sont acceptés, et au moins 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 !

Types de soumissions

Nous acceptons quatre types de soumissions :

  • Article de recherche (18 pages max.), portant sur des travaux originaux. Nous acceptons des travaux en cours, pour lesquels l'aspect recherche n'est pas entièrement finalisé. Nous encourageons aussi la soumission d'articles présentant avec élégance un résultat connu sous un angle nouveau.
  • Article court (9 pages max.), décrivant un problème particulier, les pistes en cours d'investigation, et visant à rechercher de l'aide de la part de la communauté. Les articles courts peuvent également présenter de manière synthétique et cohérente un ou plusieurs résultats déjà publié(s).
  • Tutoriel (3 pages max.), exposant clairement les objectifs et l'intérêt de la présentation, ainsi que l'environnement informatique nécessaire à sa réalisation.
  • Démonstration de logiciel (3 pages max.), décrivant l'intérêt du logiciel, qu'il soit prototypique ou abouti, ainsi que ses spécificités.

Consignes aux auteurs

  • Les articles peuvent être rédigés en français ou en anglais.
  • La forme de l'article doit être soignée, et le contenu rédigé de manière structurée et claire.
  • Le style LaTeX jflart doit impérativement être utilisé sans modification de la mise en page. Le style LaTeX et sa documentation sont disponibles ici :

    jflart.zip

  • Les limites de pages sont strictes. Les références bibliographiques ne sont pas comptabilisées dans la limite de pages. Les annexes aux articles ne sont pas autorisées.
  • Les auteurs peuvent soumettre du matériel supplémentaire, séparé de l'article soumis, sous forme de texte (version longue, sans limite de pages) et/ou de développement logiciel. L'évaluation de ce matériel supplémentaire est à la discrétion des relecteurs. Les articles soumis doivent donc être auto-contenus et évaluables sans ce matériel supplémentaire.
  • Les soumissions parallèles dans d'autres conférences, journaux ou workshops avec actes ne sont pas autorisées.
  • Les membres du comité de programme sont autorisés à soumettre un article. Les présidents du comité ne le sont pas.
  • Les articles doivent être soumis via le site :

    https://jfla2024.hotcrp.com/

  • L'évaluation des articles suit un processus en simple-aveugle : les relecteurs des articles sont anonymes, mais pas les auteurs.
  • Les articles acceptés seront publiés dans les actes de la conférence, sur HAL (portail institutionnel Inria), et les auteurs en donneront une présentation lors des journées. Les présentations seront, de préférence, données en français.

Organisation

Comité de programme

Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Rennes Présidente
Adrien Guatto IRIF, Paris Vice-président
Guillaume Baudart Inria / ENS, Paris
Sylvie Boldo Inria / LMF, Orsay
Adrien Champion OCamlPro, Paris
Arthur Charguéraud Inria, Strasbourg
Raphaëlle Crubillé CNRS / LIS, U. Aix-Marseille, Marseille
Frédéric Dabrowski LIFO / U. d'Orléans, Orléans
Pierre-Évariste Dagand CNRS / IRIF, Paris
Jean-Christophe Filliâtre CNRS / LMF, Orsay
Hugo Férée IRIF / U. Paris Cité, Paris
Chantal Keller LMF / U. Paris-Saclay, Orsay
Dominique Larchey-Wendling U. de Lorraine / CNRS / LORIA, Nancy
Assia Mahboubi Inria, Nantes
Luc Maranget Inria, Paris
Raphaël Monat Inria, Lille
Damien Pous CNRS / ENS Lyon, Lyon
Lionel Rieg Verimag / Grenoble-INP – Ensimag, Grenoble
Jocelyn Sérot Institut Pascal / U. Clermont-Auvergne, Clermont-Ferrand
Sophie Tourret Inria, Nancy
Boris Yakobowski AdaCore, Paris
Yannick Zakowski Inria, Lyon

Comité de pilotage

Zaynah Dargaye Nomadic Labs
Catherine Dubois ENSIIE
Jean-Christophe Filliâtre CNRS / LMF
Louis Mandel IBM Research
Micaela Mayero LIPN, U. Paris 13
Yann Régis-Gianas Nomadic Labs
Alan Schmitt Inria
Julien Signoles U. Paris-Saclay, CEA, List
Pierre Weis Inria

Soutiens

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

CEA LIST
GDR GPL
Mitsubishi Electric R&D Centre Europe
OcamlPro
OCaml Software Foundation
Tarides
Tweag
Université de Rennes