JFLA 2022

Journées Francophones des Langages Applicatifs
Saint-Médard-d'Excideuil
mardi 28 juin 2022

vendredi 1er juillet 2022
Domaine d'Essendiéras (Périgord)

Les actes des JFLA 2022 sont téléchargeables depuis le lien ci-dessous.

Dates importantes

Soumission des résumés 8 octobre 2021 1er octobre 2021
Soumission des articles 15 octobre 2021 8 octobre 2021
Notification aux auteurs 9 novembre 2021
Soumission version finale 7 décembre 2021
Ouverture des inscriptions 25 avril 2022 4 janvier 2022
Clôture des inscriptions 17 juin 2022 21 janvier 2022

Inscription

Pour effectuer votre inscription, veuillez suivre le lien ci-dessous, avant le vendredi 17 juin 2022 vendredi 21 janvier 2022 :

S'inscrire aux JFLA

Les inscriptions aux JFLA sont ouvertes jusqu’au 17 juin 2022. Les frais d’inscriptions seront de 660€, sauf pour les doctorants orateurs pour qui les inscriptions sont gratuites. Le paiement est possible uniquement par carte bancaire ou par bon de commande CNRS. Vos nom et prénom seront transmis à la société Rydoo.

L’inscription inclut l’hébergement, les repas et la visite de Saint-Jean-de-Côle, ainsi que le transport en navette entre la gare de Thiviers et le domaine d’Essendiéras. Veuillez indiquer lors de l’inscription si vous avez des contraintes alimentaires.

La navette entre la gare de Thiviers et le domaine d’Essendiéras partira le mardi 28 juin après l’arrivée du TER de Bordeaux de 15h03, et repartira le vendredi 1er juillet pour le TER pour Bordeaux de 10h54.

Voici des suggestions de train :

  • depuis/pour Lyon :
    • Lyon Part Dieu - Paris Gare de Lyon (TGV 6608):
      • mardi 28 juin 2022
      • départ à 8:04
      • arrivée à 10:08
    • Paris Montparnasse - Bordeaux St Jean (TGV 8255):
      • mardi 28 juin 2022
      • départ à 11:11
      • arrivée à 13:17
    • Bordeaux St Jean - Thiviers (TER 865564):
      • mardi 28 juin 2022
      • départ à 13:27
      • arrivée à 15:03
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Paris Montparnasse (TGV 8581):
      • vendredi 1er juillet 2022
      • départ à 13:47
      • arrivée à 15:53
    • Paris Gare de Lyon (TGV 6687):
      • vendredi 1er juillet 2022
      • départ à 16:58
      • arrivée à 18:56
  • depuis/pour Marseille :
    • Marseille Saint Charles - Paris Gare de Lyon (TGV 6106):
      • mardi 28 juin 2022
      • départ à 6:59
      • arrivée à 10:18
    • Paris Montparnasse - Bordeaux St Jean (TGV 8255):
      • mardi 28 juin 2022
      • départ à 11:11
      • arrivée à 13:17
    • Bordeaux St Jean - Thiviers (TER 865564):
      • mardi 28 juin 2022
      • départ à 13:27
      • arrivée à 15:03
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Paris Montparnasse (TGV 8581):
      • vendredi 1er juillet 2022
      • départ à 13:47
      • arrivée à 15:53
    • Paris Gare de Lyon - Marseille Saint Charles (TGV 6181):
      • vendredi 1er juillet 2022
      • départ à 17:07
      • arrivée à 20:11
  • depuis/pour Nantes :
    • Nantes - Bordeaux St Jean (TGV 3831):
      • mardi 28 juin 2022
      • départ à 7:55
      • arrivée à 12:07
    • Bordeaux St Jean - Thiviers (TER 865564):
      • mardi 28 juin 2022
      • départ à 13:27
      • arrivée à 15:03
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Nantes (TGV 3856):
      • vendredi 1er juillet 2022
      • départ à 13:55
      • arrivée à 18:05
  • depuis/pour Nice :
    • Nice Ville - Paris Austerlitz (TGV 5772):
      • lundi 27 juin 2022
      • départ à 19:16
      • arrivée à 7:55
    • Paris Austerlitz - Limoges Benedictins (TGV 3619):
      • mardi 28 juin 2022
      • départ à 8:29
      • arrivée à 11:57
    • Limoges Benedictins - Thiviers (TER 865561):
      • mardi 28 juin 2022
      • départ à 12:57
      • arrivée à 13:35
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Paris Montparnasse (TGV 8581):
      • vendredi 1er juillet 2022
      • départ à 13:47
      • arrivée à 15:53
    • Paris Gare de Lyon - Nice Ville (TGV 6181):
      • vendredi 1er juillet 2022
      • départ à 17:07
      • arrivée à 23:07
  • depuis/pour Paris :
    • Paris Montparnasse - Bordeaux St Jean (TGV 8255):
      • mardi 28 juin 2022
      • départ à 11:11
      • arrivée à 13:17
    • Bordeaux St Jean - Thiviers (TER 865564):
      • mardi 28 juin 2022
      • départ à 13:27
      • arrivée à 15:03
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Paris Montparnasse (TGV 8581):
      • vendredi 1er juillet 2022
      • départ à 13:47
      • arrivée à 15:53
  • depuis/pour Rennes :
    • Rennes - Paris Montparnasse (TGV 8804):
      • mardi 28 juin 2022
      • départ à 08:35
      • arrivée à 10:06
    • Paris Montparnasse - Bordeaux St Jean (TGV 8255):
      • mardi 28 juin 2022
      • départ à 11:11
      • arrivée à 13:17
    • Bordeaux St Jean - Thiviers (TER 865564):
      • mardi 28 juin 2022
      • départ à 13:27
      • arrivée à 15:03
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Paris Montparnasse (TGV 8581):
      • vendredi 1er juillet 2022
      • départ à 13:47
      • arrivée à 15:53
    • Paris Montparnasse - Rennes (TGV 8029):
      • vendredi 1er juillet 2022
      • départ à 16:57
      • arrivée à 18:25
  • depuis/pour Strasbourg :
    • Strasbourg - Paris Est (TGV 9678):
      • mardi 28 juin 2022
      • départ à 8:19
      • arrivée à 10:05
    • Paris Montparnasse - Bordeaux St Jean (TGV 8255):
      • mardi 28 juin 2022
      • départ à 11:11
      • arrivée à 13:17
    • Bordeaux St Jean - Thiviers (TER 865564):
      • mardi 28 juin 2022
      • départ à 13:27
      • arrivée à 15:03
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Massy TGV (TGV 9820):
      • vendredi 1er juillet 2022
      • départ à 12:58
      • arrivée à 15:51
    • Massy TGV - Strasbourg (TGV 5466):
      • vendredi 1er juillet 2022
      • départ à 16:27
      • arrivée à 19:01
  • depuis/pour Toulouse :
    • Toulouse Matabiau - Bordeaux St Jean (TGV 8508):
      • mardi 28 juin 2022
      • départ à 10:38
      • arrivée à 12:39
    • Bordeaux St Jean - Thiviers (TER 865564):
      • mardi 28 juin 2022
      • départ à 13:27
      • arrivée à 15:03
    • Thiviers - Bordeaux St Jean (TER 865557):
      • vendredi 1er juillet 2022
      • départ à 10:54
      • arrivée à 12:43
    • Bordeaux St Jean - Toulouse Matabiau (TGV 8505):
      • vendredi 1er juillet 2022
      • départ à 13:20
      • arrivée à 15:31

Programme

Cours invités

Delphine Demange (IRISA, Université de Rennes 1)
Si2-FIP: Programmation Fonctionnelle en Licence 1 avec Scala

Nous présentons un retour d’expérience sur un module d’enseignement de la programmation fonctionnelle en Scala, proposé ces dernières années en Licence 1 à l’Université de Rennes 1. Ce module s’adresse à un public grand débutant, qui découvre le paradigme de programmation fonctionnelle, et doit s’efforcer de déconstruire ses habitudes de programmation impérative. De fait, ce public est encore non acquis à une approche méthodique de la programmation. Dans une première partie, nous décrivons le positionnement du module dans la formation de Licence d’Informatique, ainsi que les besoins et enjeux associés, et les choix pédagogiques qui en ont résulté. Les notions enseignées dans ce module sont: la spécification et la modélisation adéquate de problèmes et des données associées, les types de données algébriques, la récursivité, l’ordre supérieur, le polymorphisme paramétrique, et les types abstraits. En seconde partie, nous illustrons de manière concrète et pratique, à l’aide d’un mini-projet proposé aux étudiants en fin de module, comment nos choix pédagogiques ont été mis en œuvre. Le projet consiste à programmer une application réactive avec interface graphique, manipulant des images représentées en interne par des arbres quaternaires, et offrant quelques transformations de base. Nous terminons par quelques éléments de réflexion pédagogique, en tirant les leçons des succès et des écueils rencontrés, et par un temps d’échange autour des besoins et des pratiques pédagogiques de la communauté.

Rust pour le formaliste impatient

Il est devenu impossible d’éviter en ligne les bruyants fans du langage de programmation Rust ces dernières années. En effet, celui-ci a été voté comme langage “le plus adoré” par Stackoverflow depuis 6 années consécutives. En tout cas, Rust a le potentiel pour plaire à la communauté des JFLAs puisqu’il possède de nombreuses fonctionnalités héritées de la programmation fonctionnelle, tout en étant orienté vers la programmation système. Mais alors, est-ce que Rust est vraiment meilleur que C++ ? Est-il possible de faire segfaulter un programme Rust ? Qu’est-ce que l’emprunt et la possession de variables ? Comment vaincre le compilateur Rust et enfin se débarrasser de ses très longs messages d’erreur ? Pour répondre à toutes ces questions, ce cours vous proposera deux sessions d’une heure trente avec un pré-requis d’un niveau M2 en méthodes formelles, afin d’aller directement au cœur du sujet et de tenter une approche fonctionnelle et formelle à la description du langage. La première session introduira les bases de la syntaxe et des fonctionnalités, notamment les concepts clés d’emprunt de possession qui permettent à Rust de garantir la sûreté mémoire statiquement. La deuxième session sera consacrée à un état de l’art de la formalisation et la vérification de programmes en Rust, dans laquelle des travaux francophones sont bien placés. Enfin, pour celles et ceux qui voudraient entrer dans l’écosystème Rust pour jouer formellement avec les programmes, un tutoriel vous apprendra à vous connecter au compilateur de Rust et récupérer les arbres de syntaxes abstraits et informations de typage dont vous auriez besoin pour vos propres projets. Pour pouvoir utiliser Rust pendant le cours, vous pouvez l’installer en suivant ces instructions : https://www.rust-lang.org/tools/install

Exposés invités

Développement d'outils audionumériques pour la création électroacoustique

En marge des systèmes de types, des preuves formelles et des systèmes de réécriture, je vous inviterai dans cet exposé ludique et largement non-scientifique à adopter un nouveau hobby: la programmation audio temps-réel embarquée. J’exposerai ici par la pratique mon activité de lutherie électronique, de la caractérisation d’un besoin musical jusqu’à la production: recherche, conception, développement logiciel et électronique, et production industrielle d’instruments et de traitements audio à destination des compositeurs et interprètes de musiques électro-acoustiques. Nous nous attarderons bien sûr — nous sommes aux JFLA — sur leur programmation, embarquée, optimisée et temps réel «dur», et l’attention particulière qu’elle exige: connaissance des caractéristiques d’exécution du processeur, du comportement du compilateur, optimisation du WCET, maîtrise précise des ressources, calculs lors de la compilation, etc. Après un survol du contexte artistique dans lequel nous nous placerons et un bref rappel de traitement du signal numérique, nous explorerons le chemin de l’information audio à travers un système embarqué typique, des doigts du musicien jusqu’aux haut-parleurs; nous détaillerons les principes et enjeux de la programmation d’un tel système temps-réel, et les techniques pratiques (ici en C++) qui rendront possible l’implémentation d’un petit instrument autonome.

En détails

lundi 28 juin

  • 17:00 — 17:25
    Adrien Guatto , Christine Tasson et Ada Vienot
    A reactive operational semantics for a lambda-calculus with time warps

    Many computer systems are reactive: they execute in continuous interaction with their environment. From the perspective of functional programming, reactive systems can be modeled and programmed as stream functions. Several lines of research have exploited this point of view. Works based on Nakano’s guarded recursion use type-theoretical modalities to guarantee productivity. Works based on synchronous programming use more specialized methods but guarantee incremental processing of stream fragments. In this paper, we contribute to a recent synthesis between the two approaches by describing how a language with a family of type-theoretical modalities can be given an incremental semantics in the synchronous style. We prove that this semantics coincides with a more usual big-step semantics.

  • 17:25 — 17:50
    Guillaume Baudart , Louis Mandel , Marc Pouzet et Reyyan Tekin
    Inférence parallèle pour un langage réactif probabiliste

    ProbZelus est un langage synchrone probabiliste qui permet de décrire des modèles probabilistes réactifs en interaction avec un environnement observable. Des méthodes d’inférences réactives permettent d’apprendre en ligne les distributions associées aux paramètres non-observés du modèle à partir d’observations statistiques. Ce problème n’a, en général, pas de solution analytique simple. Pour obtenir des estimations précises, une méthode classique consiste à analyser les résultats obtenus par de nombreuses exécutions indépendantes du modèle. Ces méthodes sont coûteuses, mais ont l’avantage de pouvoir être massivement parallélisées. Nous proposons d’utiliser JAX pour paralléliser les méthodes d’inférence réactive de ProbZelus. JAX est une bibliothèque récente qui permet de paralléliser automatiquement du code Python qui peut ensuite être exécuté de manière efficace et transparente sur CPU, GPU, ou TPU. Dans cet article, nous décrivons un nouveau moteur d’inférence réactive parallèle implémenté en JAX et le nouveau backend JAX associé pour ProbZelus. Nous montrons sur des exemples existants que notre nouvelle implémentation surpasse l’implémentation séquentielle originale pour un nombre de particules élevé.

  • 17:50 — 18:00
    Arnaud et Spiwack
    Présentation de Tweag

mardi 29 juin

  • 09:00 — 10:00
    Delphine Demange (IRISA, Université de Rennes 1)
    Si2-FIP: Programmation Fonctionnelle en Licence 1 avec Scala

    Nous présentons un retour d’expérience sur un module d’enseignement de la programmation fonctionnelle en Scala, proposé ces dernières années en Licence 1 à l’Université de Rennes 1. Ce module s’adresse à un public grand débutant, qui découvre le paradigme de programmation fonctionnelle, et doit s’efforcer de déconstruire ses habitudes de programmation impérative. De fait, ce public est encore non acquis à une approche méthodique de la programmation. Dans une première partie, nous décrivons le positionnement du module dans la formation de Licence d’Informatique, ainsi que les besoins et enjeux associés, et les choix pédagogiques qui en ont résulté. Les notions enseignées dans ce module sont: la spécification et la modélisation adéquate de problèmes et des données associées, les types de données algébriques, la récursivité, l’ordre supérieur, le polymorphisme paramétrique, et les types abstraits. En seconde partie, nous illustrons de manière concrète et pratique, à l’aide d’un mini-projet proposé aux étudiants en fin de module, comment nos choix pédagogiques ont été mis en œuvre. Le projet consiste à programmer une application réactive avec interface graphique, manipulant des images représentées en interne par des arbres quaternaires, et offrant quelques transformations de base. Nous terminons par quelques éléments de réflexion pédagogique, en tirant les leçons des succès et des écueils rencontrés, et par un temps d’échange autour des besoins et des pratiques pédagogiques de la communauté.

  • 10:00 — 10:25
    Pierre Castéran , Jérémy Damour , Karl Palmskog , Clément Pit-Claudel et Théo Zimmermann
    Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment

    Hydras & Co. is a collaborative library of discrete mathematics for the Coq proof assistant, developed as part of the Coq-community organization on GitHub. The Coq code is accompanied by an electronic book, generated with the help of the Alectryon literate proving tool. We present the evolution of the mathematical contents of the library since former presentations at JFLA meetings. Then, we describe how the structure of the project is determined by two requirements which must be continuously satisfied. First, the Coq code needs to be compatible with its ever-evolving dependencies (the Coq proof assistant and several Coq packages both from inside and outside Coq-community) and reverse dependencies (Coq-community projects that depend on it). Second, the book needs to be consistent with the Coq code, which undergoes frequent changes to improve structure and include new material. We believe Hydras & Co. demonstrates that books on formalized mathematics are not limited to providing exposition of theories and reasoning techniques—they can also provide inspiration and entertainment that transcends educational goals.

  • 10:25 — 10:40
    Adrien Champion , Steven De Oliveira et Keryan Didier
    Mikino: Induction for Dummies

    Mikino is a simple induction engine over transition systems. It is written in Rust, with a strong focus on ergonomics and user-friendliness. It is accompanied by a detailed tutorial which introduces basic notions such as logical operators and Smt solvers. Mikino and its companion tutorial target developers with little to no experience with verification in general and induction in particular. This work is an attempt to educate developers on what a proof by induction is, why it is relevant for program verification, why it can fail to (dis)prove a candidate invariant, and what to do in this case.

  • 11:00 — 12:30
    Rust pour le formaliste impatient

    Il est devenu impossible d’éviter en ligne les bruyants fans du langage de programmation Rust ces dernières années. En effet, celui-ci a été voté comme langage “le plus adoré” par Stackoverflow depuis 6 années consécutives. En tout cas, Rust a le potentiel pour plaire à la communauté des JFLAs puisqu’il possède de nombreuses fonctionnalités héritées de la programmation fonctionnelle, tout en étant orienté vers la programmation système. Mais alors, est-ce que Rust est vraiment meilleur que C++ ? Est-il possible de faire segfaulter un programme Rust ? Qu’est-ce que l’emprunt et la possession de variables ? Comment vaincre le compilateur Rust et enfin se débarrasser de ses très longs messages d’erreur ? Pour répondre à toutes ces questions, ce cours vous proposera deux sessions d’une heure trente avec un pré-requis d’un niveau M2 en méthodes formelles, afin d’aller directement au cœur du sujet et de tenter une approche fonctionnelle et formelle à la description du langage. La première session introduira les bases de la syntaxe et des fonctionnalités, notamment les concepts clés d’emprunt de possession qui permettent à Rust de garantir la sûreté mémoire statiquement. La deuxième session sera consacrée à un état de l’art de la formalisation et la vérification de programmes en Rust, dans laquelle des travaux francophones sont bien placés. Enfin, pour celles et ceux qui voudraient entrer dans l’écosystème Rust pour jouer formellement avec les programmes, un tutoriel vous apprendra à vous connecter au compilateur de Rust et récupérer les arbres de syntaxes abstraits et informations de typage dont vous auriez besoin pour vos propres projets. Pour pouvoir utiliser Rust pendant le cours, vous pouvez l’installer en suivant ces instructions : https://www.rust-lang.org/tools/install

  • 14:00 — 15:00
    Développement d'outils audionumériques pour la création électroacoustique

    En marge des systèmes de types, des preuves formelles et des systèmes de réécriture, je vous inviterai dans cet exposé ludique et largement non-scientifique à adopter un nouveau hobby: la programmation audio temps-réel embarquée. J’exposerai ici par la pratique mon activité de lutherie électronique, de la caractérisation d’un besoin musical jusqu’à la production: recherche, conception, développement logiciel et électronique, et production industrielle d’instruments et de traitements audio à destination des compositeurs et interprètes de musiques électro-acoustiques. Nous nous attarderons bien sûr — nous sommes aux JFLA — sur leur programmation, embarquée, optimisée et temps réel «dur», et l’attention particulière qu’elle exige: connaissance des caractéristiques d’exécution du processeur, du comportement du compilateur, optimisation du WCET, maîtrise précise des ressources, calculs lors de la compilation, etc. Après un survol du contexte artistique dans lequel nous nous placerons et un bref rappel de traitement du signal numérique, nous explorerons le chemin de l’information audio à travers un système embarqué typique, des doigts du musicien jusqu’aux haut-parleurs; nous détaillerons les principes et enjeux de la programmation d’un tel système temps-réel, et les techniques pratiques (ici en C++) qui rendront possible l’implémentation d’un petit instrument autonome.

  • 15:00 — 15:25
    Thibaut Benjamin , Félix Ridoux et Julien Signoles
    Formalisation d’un vérificateur efficace d’assertions arithmétiques à l’exécution

    La vérification d’assertions à l’exécution est une technique consistant à vérifier la validité d’annotations formelles au cours de l’exécution d’un programme. Bien qu’ancienne, cette technique reste encore peu étudiée d’un point de vue théorique. Cet article contribue à pallier ce manque en formalisant un vérificateur d’assertions à l’exécution pour des propriétés arithmétiques entières. La principale difficulté réside dans la modélisation d’un générateur de code pour les propriétés visées qui génère du code à la fois correct et efficace. Ainsi, le code généré repose sur des entiers machines lorsque le générateur peut prouver qu’il est correct de le faire et sur une bibliothèque spécialisée dans l’arithmétique exacte, correcte mais moins efficace, dans les autres cas. Il utilise pour cela un système de types dédié. En outre, la logique considérée pour les propriétés inclue des constructions d’ordre supérieur. L’article présente également une implémentation de ce générateur de code au sein d’E-ACSL, le greffon de Frama-C dédié à la vérification d’assertions à l’exécution, ainsi qu’une première évaluation expérimentale démontrant empiriquement l’efficacité du code généré.

  • 15:25 — 15:40
    Valentin Chaboche , Zaynah Dargaye et Arvid Jakobsson
    Soyez prudent : prenez des photos pour l'assurance avec Osnap

    Comment s’assurer que nous n’introduisons pas de bug durant l’évolution d’un logiciel ? Les outils de “snapshot testing” offrent une solution: le résultat d’une fonction est capturé et après modification comme du refactoring de code, l’outil détectera des changements indésirables. Néanmoins, le snapshot testing oblige le développeur à écrire des scénarios à la main. Nous introduisons osnap: une bibliothèque de snapshot testing avec une génération aléatoire de scénario, d’exécution, et détection de changement de comportement – inspiré par la génération aléatoire de bibliothèques comme QuickCheck en Haskell. En utilisant osnap, les développeurs peuvent sans effort générer massivement des tests de non-régression.

  • 15:40 — 15:55
    Guillaume Bury , Steven de Oliveira et Hichem Rami Ait El Hara
    Alt-Ergo-Fuzz: A fuzzer for the Alt-Ergo SMT solver

    Alt-Ergo is an open source Satisfiability Modulo Theories (SMT) solver programmed in OCaml. It was designed for program verification and is used as a back end by other software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat, the reliability of which depends on the soundness of the answers provided by Alt-Ergo and the absence of bugs in it. In this paper, we present Alt-Ergo-Fuzz, a fuzzer for Alt-Ergo which we developed with the aim of finding faults and unsoundness bugs in Alt-Ergo to solve and improve its reliability. Fuzzing is an efficient technique to test programs and find bugs. It works by quickly and automatically generating input data with which to test the software. American Fuzzy Lop (AFL) is one of the most well known and most used fuzzers in both academia and the industry. It has managed to find many bugs in various programs thanks to its grey box fuzzing technique that uses genetic algorithms and program instrumentation to generate test data that maximizes code and execution path coverage in the targeted software. By using AFL as a back end, the Crowbar OCaml library for test case generation and the CVC5 SMT solver as a reference solver of which the answers will be used to determine whether or not Alt-Ergo’s answers are correct, we managed to develop Alt-Ergo-Fuzz, which even as a work in progress and in only twenty days of testing managed to find four never found before bugs in Alt-Ergo.

  • 16:15 — 16:40
    Jean-Louis Colaço , Baptiste Pauget et Marc Pouzet
    Inférer et vérifier les tailles de tableaux avec des types polymorphes

    Cet article présente un système de vérification et d’inférence statique des tailles de tableaux dans un langage fonctionnel strict statiquement typé. Plutôt que de s’en remettre à des types dépendants, nous proposons un système de types proche de celui de ML. Le polymorphisme sert à définir des fonctions génériques en type et en taille. L’inférence permet une écriture allégée des opérations classiques de traitement du signal — application point-à-point, accumulation, projection, transposée, convolution — et de leur composition; c’est un atout clef de la solution proposée. Pour obtenir un bon compromis entre expressivité du langage des tailles et décidabilité de la vérification et de l’inférence, nous proposons une solution en deux temps : (i) un langage de types où les tailles sont des polynômes multi-variés et (ii) l’insertion de points de coercition explicites entre tailles dans le programme source. Lorsque le programme est bien typé, il s’exécute sans erreur de taille en dehors de ces points de coercitions. Deux usages de la proposition faite dans cet article peuvent être envisagés : (i) la génération de code défensif aux points de coercition ou, (ii) pour les applications critiques ou intensives, la vérification statique des coercitions en les limitant à des expressions évaluables à la compilation ou par des moyens d’analyse formelle comme l’interprétation abstraite. L’article définit le langage d’entrée, sa sémantique dynamique, son système de types et montre sa correction. Il est accompagné par une implémentation en OCaml, dont le code source est accessible publiquement.

  • 16:40 — 17:05
    Cinzia Di Giusto , Loïc Germerie Guizouarn , Ludovic Henrio et Etienne Lozes
    Formalising Futures and Promises in Viper

    Futures and promises are respectively a read-only and a write-once pointer to a placeholder in memory. They are used to transfer information between threads in the context of asynchronous concurrent programming. Futures and promises simplify the implementation of synchronisation mechanisms between threads. Nonetheless they can be error prone as data races may arise when references are shared and transferred. We aim at providing a formal tool to detect those errors. Hence, in this paper we propose a proof of concept by implementing the future/promise mechanism in Viper: a verification infrastructure, that provides a way to reason about resource ownership in programs.

  • 17:05 — 17:20
    Aymeric Fromherz et Antonin Reitz
    Démonstration de Steel, une logique de séparation concurrente pour prouver des programmes F*

    Steel est un framework pour développer et prouver des programmes concurrents écrits en F, un langage de programmation avec types dépendants ainsi qu’un assistant de preuve. Inspiré par Iris, Steel repose sur une logique de séparation concurrente imprédicative qui inclut un modèle mémoire fondé sur des monoïdes commutatifs partiels et permet l’utilisation d’invariants alloués dynamiquement pour raisonner sur des interactions concurrentes sans recourir à des verrous (“locks”). Afin d’offrir une vérification semi-automatique, Steel sépare les obligations de preuves générées en deux parties: une procédure de décision partielle, implémentée à l’aide du moteur de tactiques de F, raisonne sur la logique de séparation tandis qu’un solveur SMT permet de décharger automatiquement des obligations de preuves exprimées en logique du premier ordre, par exemple liées à de l’arithmétique. Dans cette démonstration, nous présentons plusieurs bibliothèques vérifiées qui illustrent l’expressivité et la programmabilité de Steel.

  • 17:20 — 17:35
    Çagdas Bozman , Mohamed Iguernlala , Michael Laporte , Maxime Levillain , Alain Mebsout et Sylvain Conchon
    Jouez à Faire Consensus Avec Mitten!

    Cet article présente Mitten, un outil pour décrire finement et jouer des scénarios sur une implémentation de Tenderbake — le prochain protocole de consensus “à la pBFT” de la blockchain Tezos. Mitten est paramétrable pour filtrer et examiner les messages selon des scénarios particuliers écrits dans un DSL construit sur OCaml. Grâce à Mitten, nous avons pu écrire et simuler des scénarios subtils pour reproduire des comportements difficilement atteignables en temps normal. Nous avons également pu simuler des situations permettant d’exhiber des bugs dans l’implémentation en cours et de tester des correctifs proposés.

  • 17:35 — 18:00
    Valentin Blot , Catherine Dubois et Amélie Ledein
    Vers une traduction de K en Dedukti

    K est un framework sémantique permettant de décrire formellement des sémantiques de langages de programmation. C’est aussi un environnement qui offre différents outils pour aider à la programmation avec les langages spécifiés dans le formalisme. Il est par exemple possible d’exécuter des programmes et de vérifier certaines propriétés sur ceux-ci, à l’aide de l’outil KProver. K repose sur une logique du 1er ordre munie d’une application entre formules et d’opérateurs de point fixe, d’égalité, de typage ainsi que d’un opérateur similaire à l’opérateur “next” des logiques temporelles. Ce dernier opérateur permet d’encoder la sémantique des programmes par la réécriture. Dedukti est un framework logique permettant l’interopérabilité des preuves entre différents outils de preuve formelle. Il possède des plugins d’import et d’export pour des systèmes de preuve aussi divers que Coq, PVS ou encore Isabelle/HOL. Il repose sur le LambdaPi-calcul modulo théorie, une extension de la théorie des types par l’ajout de règles de réécriture dans la relation de conversion. La flexibilité de ce logical framework permet d’encoder de nombreuses théories comme la logique du 1er ordre ou la théorie des types simples. Dans cet article, nous présentons un outil de traduction de K vers Dedukti, appelé Kamelo. Cet outil a pour objectif, à plus long terme, de permettre la vérification des preuves faites au sein de K et la réutilisation de sémantiques formelles de langages de programmation ainsi que des propriétés sur leurs programmes au sein de nombreux systèmes de preuve, via Dedukti.

mercredi 30 juin

  • 08:30 — 09:30
    Delphine Demange (IRISA, Université de Rennes 1)
    Si2-FIP: Programmation Fonctionnelle en Licence 1 avec Scala

    Nous présentons un retour d’expérience sur un module d’enseignement de la programmation fonctionnelle en Scala, proposé ces dernières années en Licence 1 à l’Université de Rennes 1. Ce module s’adresse à un public grand débutant, qui découvre le paradigme de programmation fonctionnelle, et doit s’efforcer de déconstruire ses habitudes de programmation impérative. De fait, ce public est encore non acquis à une approche méthodique de la programmation. Dans une première partie, nous décrivons le positionnement du module dans la formation de Licence d’Informatique, ainsi que les besoins et enjeux associés, et les choix pédagogiques qui en ont résulté. Les notions enseignées dans ce module sont: la spécification et la modélisation adéquate de problèmes et des données associées, les types de données algébriques, la récursivité, l’ordre supérieur, le polymorphisme paramétrique, et les types abstraits. En seconde partie, nous illustrons de manière concrète et pratique, à l’aide d’un mini-projet proposé aux étudiants en fin de module, comment nos choix pédagogiques ont été mis en œuvre. Le projet consiste à programmer une application réactive avec interface graphique, manipulant des images représentées en interne par des arbres quaternaires, et offrant quelques transformations de base. Nous terminons par quelques éléments de réflexion pédagogique, en tirant les leçons des succès et des écueils rencontrés, et par un temps d’échange autour des besoins et des pratiques pédagogiques de la communauté.

  • 09:30 — 09:55
    Nicolas Chataing , Camille Noûs et Gabriel Scherer
    Déboîter les constructeurs

    Nous proposons une implémentation d’une nouvelle fonctionnalité pour OCaml, le déboîtement de constructeurs. Elle permet d’éliminer certains constructeurs de la représentation dynamique des valeurs quand cela ne crée pas d’ambiguité entre différentes valeurs au même type. Nous décrivons:

    • un cas d’usage sur les grands entiers où la fonctionnalité améliore les performances de code OCaml idiomatique, éliminant le besoin d’écrire du code non-sûr,

    • l’analyse statique nécessaire pour accepter ou rejeter le déboîtement d’un constructeur,

    • et l’impact sur la compilation du filtrage de motif. Pour notre analyse statique, nous devons normaliser certaines expressions de type, avec une relation de normalisation qui ne termine pas nécessairement en présence de types mutuellement récursifs. Nous décrivons une analyse de terminaison qui garantit la normalisation sans rejeter les déclarations de types qui nous intéressent.

  • 09:55 — 10:10
    Léo Andrès , Raja Boujbel , Louis Gesbert et Dario Pinto
    Connecter l'écosystème OCaml à Software Heritage via opam

    Software Heritage est un projet initié par Inria ayant pour but d’archiver l’ensemble des logiciels libres disponibles sur internet. On présente dans cet article Software Heritage et on y décrit les travaux effectués et en cours en lien avec l’écosystème OCaml, opam et Software Heritage. Ces travaux comprennent notamment l’ajout à Software Heritage de modules permettant l’archivage des paquets présents sur opam, le développement d’une bibliothèque OCaml permettent de travailler avec les identifiants Software Heritage, l’ajout à opam de la possibilité de récupérer sur Software Heritage des paquets qui ne sont plus disponibles et enfin la correction du dépôt opam officiel afin de retrouver les paquets déjà manquants. Aujourd’hui, 3516 paquets opam sont déjà archivés sur Software Heritage.

  • 10:30 — 12:00
    Rust pour le formaliste impatient

    Il est devenu impossible d’éviter en ligne les bruyants fans du langage de programmation Rust ces dernières années. En effet, celui-ci a été voté comme langage “le plus adoré” par Stackoverflow depuis 6 années consécutives. En tout cas, Rust a le potentiel pour plaire à la communauté des JFLAs puisqu’il possède de nombreuses fonctionnalités héritées de la programmation fonctionnelle, tout en étant orienté vers la programmation système. Mais alors, est-ce que Rust est vraiment meilleur que C++ ? Est-il possible de faire segfaulter un programme Rust ? Qu’est-ce que l’emprunt et la possession de variables ? Comment vaincre le compilateur Rust et enfin se débarrasser de ses très longs messages d’erreur ? Pour répondre à toutes ces questions, ce cours vous proposera deux sessions d’une heure trente avec un pré-requis d’un niveau M2 en méthodes formelles, afin d’aller directement au cœur du sujet et de tenter une approche fonctionnelle et formelle à la description du langage. La première session introduira les bases de la syntaxe et des fonctionnalités, notamment les concepts clés d’emprunt de possession qui permettent à Rust de garantir la sûreté mémoire statiquement. La deuxième session sera consacrée à un état de l’art de la formalisation et la vérification de programmes en Rust, dans laquelle des travaux francophones sont bien placés. Enfin, pour celles et ceux qui voudraient entrer dans l’écosystème Rust pour jouer formellement avec les programmes, un tutoriel vous apprendra à vous connecter au compilateur de Rust et récupérer les arbres de syntaxes abstraits et informations de typage dont vous auriez besoin pour vos propres projets. Pour pouvoir utiliser Rust pendant le cours, vous pouvez l’installer en suivant ces instructions : https://www.rust-lang.org/tools/install

  • 17:35 — 18:00
    François Bobot et Arthur Correnson
    Un Coq apprend à un bébé colibri à flotter

    L’arithmétique flottante est connue pour être un sujet difficile. Ses propriétés contre-intuitives rendent l’écriture d’algorithmes manipulant les nombres flottants propice à de nombreuses erreurs. Des outils automatiques pour la vérification de programmes flottants existent mais ces outils mobilisant eux-même du calcul flottant, on peut se poser la question de leur propre fiabilité. Pour adresser ce problème, nous proposons de vérifier formellement l’implémentation de raisonnements sur les nombres flottants dans un solveurs CP. En particulier, nous discutons d’une méthodologie pour mener les preuves en utilisant l’assistant de preuve Coq. Nous discutons également de l’intégration des raisonnements prouvés à un développement logiciel complet en OCaml.

  • 18:00 — 18:15
    Denis Cousineau , Enzo Crance et Assia Mahboubi
    Trakt : Uniformiser les types pour automatiser les preuves

    Dans un assistant de preuve comme Coq, un même objet mathématique peut souvent être formalisé par différentes structures de données. Par exemple, le type Z des entiers binaires, dans la bibliothèque standard de Coq, représente les entiers relatifs tout comme le type ssrint, des entiers unaires, fourni par la bibliothèque MathComp. En pratique, cette situation familière en programmation est un frein à la preuve formelle automatique. Dans cet article, nous présentons trakt, un outil dont l’objectif est de faciliter l’accès des utilisateurs de Coq aux tactiques d’automatisation, pour la représentation des théories décidables de leur choix. Cet outil construit une formule auxiliaire à partir d’un but utilisateur, et une preuve que cette dernière implique ce but initial. La formule auxiliaire est conçue pour être adaptée aux outils de preuve automatique (lia, smtcoq, etc). Cet outil est extensible, grâce à une API permettant à l’utilisateur de définir plusieurs natures de plongements dans un jeu de structures de données de références. Le méta-langage coq-elpi, utilisé pour l’implémentation, fournit des facilités bienvenues pour la gestion des lieurs et la mise en œuvre des parcours de termes en jeu dans ces tactiques.

  • 18:15 — 18:30
    Valentin Blot , Louise Dubois de Prisque , Chantal Keller et Pierre Vial
    Bécassine à la chasse au Coq

    Nous présentons une nouvelle tactique Coq snipe permettant de prouver automatiquement des buts Coq en les envoyant à des prouveurs automatiques externes du premier ordre via des plugins. Pour ce faire, la tactique snipe réduit le but à un énoncé du premier ordre et enrichit le contexte local avec des énoncés explicitant pour le prouveur la sémantique du but. Nous combinons des transformations modulaires et indépendantes permettant chacune de réduire un aspect spécifique du langage de Coq au langage (plus simple) d’un prouveur automatique. A l’heure actuelle, snipe utilise des transformations simples mais cruciales qui explicitent des définitions et des types algébriques. Ceci permet de prouver automatiquement des buts mêlant raisonnement au premier ordre, types de données et polymorphisme. Ce prototype de tactique automatique est un premier pas vers l’implantation et la combinaison de transformations plus complexes, qui rendront Coq plus facile d’accès.

  • 18:30 — 18:45
    Pierre Roux
    Number Notation dans Coq

    L’assistant de preuve Coq dispose d’une fonctionnalité permettant à l’utilisateur de définir ses propres notations avec une grande souplesse. Dans ce cadre, les constantes numériques étaient initialement interprétées et affichées par du code dédié dans des plugins OCaml. Depuis Coq 8.9, la commande Numeral Notation (aujourd’hui renommée Number Notation) permet d’implémenter ces parsers et printers de constantes numériques directement dans Coq. Suite entre autre à l’introduction des flottants primitifs, cette commande a depuis connue un certain nombre d’extensions qui seront présentées dans cette démonstration : valeurs à virgules ou exposant, valeurs hexadécimales, interprétation vers des types inductifs paramétrés ou non inductifs.

  • 18:45 — 19:00
    Pablo Donato , Pierre-Yves Strub et Benjamin Werner
    Actema : une interface graphique et gestuelle pour preuves formelles

    Nous proposons de présenter un prototype expérimental de nouvelle interface utilisateur graphique pour construire des preuves formelles. Cette interface permet de construire les preuves à travers des actions effectuées sur les éléments du but (hypothèses et conclusion). En particulier elle étend l’approche de proof-by-pointing développée dans les années 1990 avec des actions par glisser-déposer (Drag-and-drop).

jeudi 1er juillet

  • 08:30 — 08:45
    Emmanuel Chailloux , Jocelyn Sérot et Loïc Sylvestre
    Macle : un langage dédié à l'accélération de programmes OCaml sur circuits FPGA

    Les circuits reprogrammables de types FPGA constituent un matériel de choix pour la réalisation d’accélérateurs de calculs. L’implémentation O2B de la machine virtuelle OCaml permet d’appeler des circuits externes réalisés sur FPGA depuis un langage de haut niveau (OCaml) compilé en byte code. La conception de circuits s’appuie sur des langages de description de matériel (HDL) souvent fort éloignés des langages algorithmiques. C’est pourquoi l’on présente Macle, un langage applicatif dédié à la programmation de calculs séquentiels et parallèles synthétisables en circuits. On décrit la chaîne de compilation de Macle vers un HDL et son intégration à O2B.

  • 08:45 — 09:10
    Alain Delaet et Denis Merigoux
    Catala, un langage pour transformer la loi en code

    Le droit codifie et régit de nombreux aspects de la vie quotidienne. Si la plupart du temps les lois sont sujettes à interprétation, dans certains domaines la loi ne permet pas d’interprétation et vise essentiellement à décrire rigoureusement un calcul ou une procédure de décision, c’est-à-dire un algorithme. Catala est un nouveau langage conçu en collaboration avec des juristes qui permet une compilation depuis une spécification proche de la loi vers un code exécutable. Contrairement aux langages traditionnels, Catala est adapté aux raisonnements cas de base/exceptions présents dans la loi; il intègre de la programmation littéraire du droit qui facilite les mises à jour du programme. Finalement, Catala compile vers une variété de langages cibles dont OCaml. Dans cette présentation de prototype, nous montrerons comment exprimer une partie du calcul des allocations familliales dans Catala.

Appel à soumission

Les 33es Journées Francophones des Langages Applicatifs (JFLA) se tiendront à Saint-Médard-d'Excideuil, plus précisément Domaine d'Essendiéras (Périgord) , du mardi 28 juin 2022 au vendredi 1er juillet 2022 .

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 quatre types de soumissions :

  • Article de recherche de seize pages au plus (hors bibliographie) , 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 (hors bibliographie) , pour rechercher de l'aide pour résoudre un problème particulier, ou reparler d'un papier déjà publié.
  • Proposition de tutoriel d'une page (hors bibliographie) exposant son intérêt et ses objectifs ainsi que l'environnement informatique nécessaire à sa réalisation.
  • Proposition de démonstration d'un outil ou d'un prototype de deux pages (hors bibliographie) décrivant pourquoi ce logiciel est intéressant ainsi que ses spécificités.

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. Les tutoriels auront un créneau de vingt-cinq minutes et les démonstrations d'outils ou de prototypes se verront allouer quinze minutes.

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.

Le style LaTeX Easychair doit être respecté :

https://easychair.org/publications/for_authors

Les soumissions se font sur la page Easychair des JFLA :

https://easychair.org/conferences/?conf=jfla22

Organisation

Comité de programme

Chantal Keller LMF, Université Paris-Saclay Présidente
Timothy Bourke Inria, ÉNS de Paris Vice-président
Sandrine Blazy Irisa, Université Rennes 1
Frédéric Bour Tarides - Inria
Guillaume Bury OcamlPro
Stefania Dumbrava Samovar, ENSIIE, Télécom Sud Paris
Diane Gallois-Wong Nomadic Labs
Adrien Guatto IRIF, Université de Paris
David Janin LaBRI, Université de Bordeaux
Marie Kerjean LIPN, Université Paris 13
Luc Pellissier LACL, Université Paris-Est Créteil
Mário Pereira NOVA-LINCS, Universidade Nova de Lisboa
Alix Trieu Aarhus University
Yannick Zakowski LIP, Inria, ÉNS de Lyon

Comité de pilotage

Zaynah Dargaye Nomadic Labs
Catherine Dubois École Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)
Jean-Christophe Filliâtre CNRS
Louis Mandel IBM Research
Micaela Mayero LIPN, Université Paris 13
Yann Régis-Gianas Nomadic Labs
Alan Schmitt Inria Rennes - Bretagne Atlantique
Julien Signoles CEA LIST
Pierre Weis Inria Paris

Soutiens

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