index - Trente-Cinquièmes Journées Francophones des Langages Applicatifs

Ce site web réunit les articles des JFLA 2024.
Tous les articles et les actes de la conférence ont été déposés sur HAL (portail institutionnel Inria).

Le site web de la conférence contient les informations pour l'évènement lui-même.

Vous pouvez accéder à tous les articles :

  • directement depuis le site web de la conférence, dans la section "Programme"
  • ou bien depuis ici, en consultant les deux onglets "Publications" et "Publications (par auteur)"

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.
  • 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.

Exposés invités

  • Utilisation de Coq pour l'enseignement des mathématiques en L1 et en seconde. Marie Kerjean, Micaela Mayero et Pierre Rousselin.
  • Infer: a compositional and extensible platform for static analysis. Jules Villard.
  • MetaCoq : de la métaprogrammation à l’extraction certifiée pour Coq. Matthieu Sozeau.
  • Programmation réactive probabiliste. Guillaume Baudart et Christine Tasson.

Articles sélectionnés

Structures de données

  • De l’avantage de nuancer les décisions binaires. Claude Marché et Denis Cousineau.
  • Comparing EventB, {log} and Why3 Models of Sparse Sets. Maximiliano Cristiá and Catherine Dubois.
  • Rough Pearl: Manufacturing Cons-Cells. Pierre-Évariste Dagand, Pierre Letouzey, and Ellenor Fatemeh Taghayor.

Sûreté du logiciel

  • Réutilisations de caches et d’invariants pour l’analyse statique incrémentale. Mamy Razafintsialonina, David Bühler, Antoine Miné, Valentin Perrelle et Julien Signoles.
  • Alias : pointeurs espionnés en série. Tristan Le Gall, Jan Rochel, Florian Faissole, Julien Signoles et Denis Cousineau.
  • À la recherche de tous les vrais bugs - Verification formelle d’un détecteur de bugs automatique. Arthur Correnson.
  • Correct tout seul, sûr à plusieurs. Clément Allain et Gabriel Scherer.

Compilation

  • Chamelon : un minimiseur pour et en OCaml. Milla Valnet, Nathanaëlle Courant, Guillaume Bury, Pierre Chambart et Vincent Laviron.
  • Correct, Fast LR(1) Unparsing. François Pottier.
  • Source-to-Source Optimizations Validated using Separation Logic. Guillaume Bertholon, Arthur Charguéraud, and Thomas Kœhler.
  • Chamois: agile development of CompCert extensions for optimization and security. David Monniaux and Sylvain Boulmé.
  • L’interprète, le JIT et la licorne. Frédéric Recoules et Sébastien Bardin.

Sémantique

  • Resource Categories from Differential Categories. Lison Blondeau-Patissier.
  • Skeletal Semantics of a Fragment of Python. Martin Andrieux and Alan Schmitt.
  • Liveness Properties in Geometric Logic for Domain-Theoretic Streams. Colin Riba and Solal Stern.
  • Executable semantics of Arm’s Architecture Specification Language. Hadrien Renaud.
  • Towards a linear functional translation for borrowing. Sidney Congard.

Langages de programmation

  • Type Inference of Polymorphic and Overloaded Functions. Towards Static Typing of Dynamic Languages. Mickaël Laurent.
  • Stimulus: un langage synchrone à contraintes. Bertrand Jeannet, Étienne Closse, Fabien Gaucher et Daniel Weil.
  • Un prototype de système de types graduels ensemblistes pour Elixir. Guillaume Duboc.
  • Destination-passing style programming: a Haskell implementation. Thomas Bagrel.
  • Modular efficient deconstruction with typed pointer reversal. Jean Caspar and Guillaume Munch-Maccagnoni.

Preuve formelle, ingénierie de la preuve

  • Towards the Fundamental Theorem of Calculus for the Lebesgue Integral in Coq. Reynald Affeldt and Zachary Stone.
  • Packaging Proofs with Why3find. Loïc Correnson.
  • A diagram editor to mechanise categorical proofs. Ambroise Lafont.


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