JFLA 2025

Journées Francophones des Langages Applicatifs
lieu-dit Saint Hilaire, Roiffé
mardi 28 janvier 2025
vendredi 31 janvier 2025
Domaine de Roiffé
Vue diurne des façades du Domaine de Roiffé

Dates importantes

Soumission des résumés et articles 16 octobre 2024
Notification aux auteurs 3 décembre 2024
Envoi des versions finales 17 décembre 2024
Inscriptions 4 décembre 2024 - 7 janvier 2025
Conférence 28 janvier 2025 - 31 janvier 2025

Inscription

Pour effectuer votre inscription, veuillez suivre le lien ci-dessous, avant le mardi 7 janvier 2025 :

S'inscrire aux JFLA

Type d'inscription Montant T.T.C.
Chambre double 590 €
Chambre simple (nombre limité) 670 €
Étudiant·e orateur·ice pour un article accepté (stagiaire de master, personne inscrite en thèse) (chambre double) 0 €
Inscription subventionnée (voir conditions spécifiques) (chambre double) 0 €

Les chambres simples étant disponibles en nombre limité, nous vous demandons de préférer l’inscription en chambre double si possible.


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

Ces frais couvrent l’aller-retour en autocar entre Tours et le Domaine de Roiffé (voir ci-dessous), le logement en chambre individuelle ou double du lundi 27 janvier au vendredi 31 janvier (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.

La plateforme Azur Colloque du CNRS gère le processus d’inscription et de règlement des frais aux JFLA 2025.

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


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

Les JFLA 2025 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 en chambre double (soit 590 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 le sont pour nous permettre de réaliser les arbitrages nécessaires.

Les candidatures sont recevables jusqu'au vendredi 27 décembre 2024.
Les notifications de subvention (accord ou refus) seront communiquées individuellement au plus tard le jeudi 2 janvier 2025.

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 Tours - Domaine de Roiffé [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 Tours et le Domaine de Roiffé en autocar (1h15 de trajet). Elle passera par la gare de Saint-Pierre-des-Corps.

  • Aller : lundi 27 janvier, départ de la gare routière de Tours à 18h15, passage par la gare de Saint-Pierre-des-Corps à 18h30, arrivée au domaine à 19h30.
  • Retour : vendredi 31 janvier, départ du domaine à 13h30, passage par la gare de Saint-Pierre-des-Corps, arrivée à Tours à 14h45.


Programme

Exposés invités

Laure Gonnord (Université Grenoble Alpes, Grenoble INP, LCIS) et Gabriel Radanne (Inria)
Optimising data types for fun and performance

Initially present only in functional languages such as OCaml and Haskell, Algebraic Data Types (ADTs) have now become pervasive in mainstream languages, providing nice data abstractions and an elegant way to express functions through pattern matching. Unfortunately, ADTs remain seldom used in low-level programming. One reason is that their increased convenience comes at the cost of abstracting away the exact memory layout of values. Even Rust, which tries to optimize data layout, severely limits control over memory representation.

In this talk, I will present two contributions whose goal are to let programmers specify highly optimized memory layouts for inductive data structures in a flexible and expressive way, while still enjoying high-level programming constructs such as ADTs and pattern matching to manipulate this data.

In the context of Thaïs Baudon’s Phd thesis, we developped a language dubbed ribbit which combines a high-level language, consisting of ADTs, pattern matching and basic manipulation of immutable values, with memory types specifying the precise memory layout of each high-level type, providing full control over the memory representation of values. The language comes with a proven-correct compilation process. This work was partially published at ICFP2023.

We also explored, in the context of Paul Iannetta’s Phd thesis, the optimisation of programs operating on mutable terms stored as arrays. Such representation could take advantage of parallelism opportunities that appear in tree-like structures. We present the language REW, a prototype language with pattern matching, and its compilation process, as a first step to compile pattern matching as parallel in-place modifications of the underlying memory representation. This work was partially published at GPCE 2021.

Hugo Herbelin (Inria)
Calculer avec l'axiome du choix et ses variantes

On peut sans doute dire que l’axiome du choix dans toute sa généralité est le dernier axiome logique standard dont on ne sait pas encore décrire en termes très clairs le contenu calculatoire.

Nous essayerons alors dans cet exposé de synthétiser l’état de l’art dont nous avons connaissance sur la question. En particulier, après un rappel des correspondances de base entre axiomes logiques et concepts de programmation (tel que logique classique = callcc), un rappel de la taxonomie des différentes formes de choix et de leur rôle en mathématiques (Zorn, choix dépendant, récurrence barrée, récurrence bien fondée, lemme de König, décalage de la double négation, thèse de Church, principe de continuité, …), nous décrirons quelques unes des briques de programmation permettant, à défaut de couvrir toute la généralité de l’axiome du choix, de calculer avec certaines variantes de choix, notamment la « récursion barrée » (une distributivité des monades fortes sur les streams) et le « quote » (une primitive d’introspection de code).

Didier Rémy (Inria)
Enseignement de la programmation fonctionnelle en M2 : à la recherche d'un équilibre entre théorie et pratique
Jocelyn Sérot (Université Clermont Auvergne)
Pourquoi les gens qui font du logiciel sérieusement devraient construire leur propre matériel

On réinterprétera cette phrase d’A. Kay des années 80 dans le contexte des architectures matérielles d’aujourd’hui, et en particulier des possibilités offertes par les circuits reprogrammables de type FPGA (Field Programmable Gate Arrays). On s’attachera notamment à montrer en quoi les concepts fondamentaux qui sous-tendent l’utilisation de ces circuits s’éloignent de ceux qui fondent la programmation des micro-processeurs. Mais aussi comment l’usage de modèles et de langages de programmation adéquats permettent de réduire le fossé ainsi créé et, dès lors, de permettre à des programmeurs non-spécialistes des architectures d’exploiter toutes les potentialités offertes par les circuits FPGA.

L’exposé comprendra deux parties : une première essentiellement didactique, visant à introduire les notions clés en conception de matériel (architecture interne des FPGA, horloges, niveau transfert de registres, langages de description de matériel, synthèse logique, …) et une deuxième présentant quelques solutions répondant aux objectifs sus-cités, certaines issues des travaux de l’auteur.


Articles acceptés

La liste des articles acceptés aux JFLA est la suivante.

Articles de recherche
Guillaume Bertholon et Arthur Chargueraud
Bidirectional Translation between a C-like Language and an Imperative Lambda-calculus
Pierre-Evariste Dagand , Jean-Baptiste Menant et Yves Ndiaye
Can Symmetric Cryptography Be Liberated from the Von Neumann Style?
Yves Bertot et Thomas Portet
Chassez le naturel dans la formalisation des mathématiques
Michele Alberti , François Bobot , Zakaria Chihani , Julien Girard-Satabin , Alban Grastien et Aymeric Varasse
Composer une salade CAISAR avec des réseaux de neurones et de l’édition de graphe
Léo Andrès et Zhicheng Hui
Cross-Language Symbolic Runtime Annotation Checking
Josué Moreau
Des briques de calcul formel plus solides avec Capla
Quentin Vermande
Décomposition Algébrique Cylindrique en Coq/Rocq
Anne Grieu et Jean-Paul Bodeveix
Encodage du langage mathématique d’Event-B dans Lambdapi
Jean-Christophe Filliâtre , Andrei Paskevich et Henri Saudubray
Faire chauffer Why3 avec de l’induction
Jérémy Damour , Allan Blanchard , Loïc Correnson et Frédéric Loulergue
Formalisation d’une analyse de région pour Frama-C/WP
Samuel Arsac , Damien Pous et Russ Harmer
Formalizing adhesive category theory in Rocq
Hugo Férée , Sam van Gool et Yago Iglesias Vazquez
Formulas Rewritten And Normalized Computationally, And Intuitionistically Simplified
Benoît Ballenghien
HOL-CSP : des erreurs à rattraper
Louis Gesbert
L'explication par la paresse
Charlène Gros et Mário Pereira
Le chameau et le serpent rentrent dans un bar : vérification quasi-automatique de code OCaml en logique de séparation
Reynald Affeldt
Prouver que π est irrationnel avec MathComp-Analysis
Basile Gros , Pierre Corbineau et Jean-François Monin
Proxy-based small inversions : a case study in MetaCoq programming
Stefan Monnier
Reconciling Impredicative Axiom and Universe
Benjamin Bonneau
Relational reasoning on monadic semantics
Paul Patault , Xavier Denis et Arnaud Golfouse
Remonter les barrières pour ouvrir une clôture
David Monniaux et Sylvain Boulmé
Safe external calls from formally verified functional code: exiting the monad, and a BDD case study
Basile Clément et Gabriel Scherer
Storable types: free, absorbing, custom
Zacharie Moughanim et Lionel Vaux Auclair
The weak algebraic lambda-calculus
Arthur Charguéraud , Martin Bodin et Louis Riboulet
Typechecking of Overloading in Programming Languages and Mechanized Mathematics
Thierry Marianne , Fred Mesnard et Étienne Payet
Vers une automatisation de la certification des propriétés de clôture pour Prolog
Paul Geneau de Lamarlière
Vérification de bout en bout d'une fonction de bibliothèque mathématique
Clément Allain
Zoo: A framework for the verification of concurrent OCaml 5 programs using separation logic

Appel à soumission

Les 36es Journées Francophones des Langages Applicatifs (JFLA) se tiendront au lieu-dit Saint Hilaire, Roiffé, plus précisément au Domaine de Roiffé , du mardi 28 janvier 2025 au vendredi 31 janvier 2025 .

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, 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.
  • Questions d'enseignement, de formation, ou de diffusion des langages fonctionnels et applicatifs. Environnements et méthodes 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 deux types de soumissions :

  • Article de recherche (18 pages maximum), 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 maximum), 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. Enfin, ils peuvent présenter un outil logiciel dont l'exposé constituera une démonstration.

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://jfla2025.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

Adrien Guatto IRIF, Université Paris Cité Président
Marie Kerjean LIPN, CNRS Vice-présidente
Reynald Affeldt AIST
Aurore Alcolei LACL, Université Paris-Est Créteil
Guillaume Baudart IRIF, Inria Paris
Raja Boujbel OCamlPro
Adrien Champion Anzenlang
Arthur Charguéraud Inria, Université de Strasbourg
Évelyne Contejean LRI, CNRS
Armaël Guéneau LMF, Inria Saclay
Tom Hirschowitz LAMA, CNRS and Université Savoie Mont Blanc
Ambroise Lafont LIX, École polytechnique
Étienne Miquey I2M, Aix-Marseille Université
Stefan Monnier Université de Montréal
Denis Mérigoux Inria Paris
Frédéric Peschanski LIP6, Sorbonne Université
Basile Pesin VERIMAG, Université Grenoble Alpes
Cécilia Pradic Université de Swansea
Xavier Rival DIENS, Inria Paris
Julien Signoles Université Paris-Saclay, CEA, LIST
Arnaud Spiwack Tweag
Yannick Zakowski LIP, Inria Lyon

Volontaires étudiant·e·s

Adrienne Lancelot IRIF, Inria Paris

Comité de pilotage

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