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
|
Comité de pilotage
|