JFLA 2020

Gruissan village, la nuit
Gruissan Tour Barberousse
Gruissan village, la nuit
Gruissan
mercredi 29 janvier 2020

samedi 1er février 2020

Dates importantes

Soumission des résumés 4 octobre 2019 1er octobre 2019
Soumission des articles 15 octobre 2019 8 octobre 2019
Notification aux auteurs 9 novembre 2019 2 novembre 2019
Clôture des inscriptions 8 janvier 2020

Inscription

Pour effectuer votre inscription, veuillez suivre le lien ci-dessous, avant le mercredi 8 janvier 2020 :

S'inscrire aux JFLA

L’inscription est gratuite pour les étudiant.e.s orateur.e.s (en chambre double) et de 600 euros pour les autres (en chambre simple).

Elle inclut l’hébergement et les repas, ainsi que le transport en navette entre la gare de Narbonne et l’hôtel Phoebus Garden & Spa.

Voici les trains suggérés depuis/pour Paris :

  • Paris Gare de Lyon - Narbonne (TGV INOUI 6275):
    • mercredi 29 janvier 2020
    • départ à 11:08
    • arrivée à 15:34
  • Narbonne - Paris Gare de Lyon (RENFE SNCF 9702):
    • samedi 1er février 2020
    • départ à 12:20
    • arrivée à 16:45

Les informations concernant les liaisons avec les navettes gare de Narbonne / hôtel Phoebus vous seront précisées ultérieurement.

Programme

Cours invités

Sylvain Conchon (LRI, Université Paris-Saclay)
Cubicle: Model Checking Modulo Théories
Claire Dross (AdaCore)
SPARK 2014: La Preuve de Programme pour les Développeurs

Exposés invités

Pierre-Évariste Dagand (CNRS, INRIA, Sorbonne Université)
L'expérience Usuba : un compilateur post-Moore
Hugo Herbelin (INRIA Paris, IRIF)
Titre à venir ...

Articles acceptés

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

Articles de recherche
Esaïe Bauer et Marie Kerjean
Chiralités et exponentielles: un peu de différentiation

Nous donnons une sémantique catégorique à la logique linéaire différentielle finitaire et polarisée. Cette axiomatique propose une axiomatique pour des modèles polarisés précédemment mis à jour dans les espaces vectoriels topologiques. Elle s’appuie sur la notion de chiralités de Melliès et sur les modèles non-polarisé de la logique linéaire différentielle munis d’un biproduit de Fiore.

David Janin , Bernard Serpette et Simon Archipoff
Des promesses, des actions, par flots, en OCaml

Nous nous intéressons aux traitements de flux audio synchrones et aux contrôles de ces traitements par des flux de commandes asynchrones : un exemple archétypal de problème de programmation globalement asynchrone et localement synchrone (GALS). Pour faire cela, un modèle qui s’impose tout à la fois par son efficacité et son élégance se situe à la croisée de plusieurs concepts clés de la programmation fonctionnelle : les actions monadiques, les promesses, et les flots récursifs d’actions ou de promesses. Suite à une expérimentation de cette modélisation en Haskell, l’objet de cet article est d’en faire une expérimentation en OCaml. De façon quelque peut inattendue, les deux approches se complètent et nous conduisent finalement à une axiomatisation originale de la notion de promesse. De plus, étendu aux flots récursifs d’actions, il apparaît que les promesses de flots d’actions peuvent être vue comme des flots de promesses. Une mise en oeuvre de ces concepts est proposée en s’appuyant sur l’extension d’OCaml par threads Unix.

Quentin Garchery , Chantal Keller , Claude Marché et Andrei Paskevich
Des transformations logiques passent leur certificat

Dans un contexte de vérification formelle de programmes, utilisant des démonstrateurs automatiques, la base de confiance des environnements de vérification est typiquement très large. Ainsi, un outil de vérification de programmes tel que Why3 comporte de nombreuses procédures complexes: génération de conditions de vérification, transformations logiques de tâches de preuve et interactions avec des démonstrateurs externes. En ne considérant que les transformations logiques dans Why3, leur implantation comporte déjàplus de 17000 lignes de code OCaml. Afin d’augmenter notre confiance dans la correction d’un tel outil de vérification, nous proposons un mécanisme de transformations certifiantes, produisant des certificats pouvant être validés par un outil externe, selon l’approche sceptique. Nous présentons ce mécanisme de génération de certificats et explorons deux méthodes pour les valider: une fondée sur un vérificateur dédié développé en OCaml, l’autre reposant sur le vérificateur de preuves universel Dedukti. Une spécificité de nos certificats est d’être «à petits grains» et composables, ce qui rend notre approche incrémentale, permettant d’ajouter graduellement de nouvelles transformations certifiantes.

Alexandre Moine et Yann Regis-Gianas
Détection de définitions OCaml similaires (ou comment ne plus voir - double à dos de chameau)

L’absence de redondance est souvent un gage de qualité pour un code source. En effet, lorsqu’un fragment de code est répété, ses imperfections – pour ne pas dire ses erreurs – le sont elles-aussi. Seulement, il arrive parfois que l’on constate de la redondance dans un grand corpus de code, typiquement quand ce corpus a été construit par des développeurs ne communiquant peu ou pas du tout entre eux. Deux instances de cette situation nous intéressent particulièrement : l’ensemble des codes sources des paquets OPAM et l’ensemble des copies d’étudiants répondant tous aux mêmes questions de programmation. Comment partitionner leurs définitions en fonction de leur similarité''? Dans cet article, nous proposons un outil de partitionnement automatique d'un ensemble de définitions écrites en OCaml. Cet outil s'appuie sur une fonction dédiée dehachage’’ des arbres de syntaxe du langage intermédiaire Lambda ainsi que sur un algorithme de classification hiérarchique classique que nous avons adapté à notre usage. Cet outil prend la forme d’une bibliothèque nommée Asak disponible sur OPAM. Nous l’avons utilisé d’une part pour partitionner automatiquement les réponses d’étudiants qui apprennent OCaml en utilisant la plateforme LearnOCaml, et d’autre part, pour détecter des redondances sur l’ensemble des codes sources des paquets OPAM disponibles aujourd’hui. Nous évaluons les résultats obtenus et formulons les limites de notre approche.

Amélie Ledein et Catherine Dubois
FaCiLe en Coq : vérification formelle des listes d'intervalles

Lors du développement d’ un solveur de contra!ntes, la représentation des domaines des variables est un choix de conception important car ce dernier a une forte influence sur l’efficacité du solveur. Une représentation assez courante - et judicieuse lorsque les domaines sont grands et “avec peu de trous” - consiste à stocker une séquence d’intervalles aussi larges que possible. La bibliothèque OCaml FaCiLe de Programmation par Contraintes sur les domaines finis (Barnier, Brisset, 1997) ainsi que de nombreux autres solveurs, implantent les domaines avec une telle représentation. Nous présentons dans cet article la formalisation en Coq du module de FaCiLe dédié à la création et la manipulation des domaines. Dans ce travail, l’effort a porté non seulement sur la preuve mais surtout sur la spécification des fonctions de ce module. Plus généralement, nous proposons une nouvelle implantation Coq des ensembles finis d’entiers. Notre objectif est d’utiliser le module Coq correspondant dans le solveur de contraintes formellement vérifié développé par Carlier et al, afin d’obtenir de meilleures performances pour le code extrait. Ce travail participe également à l’effort de vérification formelle des bibliothèques OCaml existantes.

Louis Noizet et Alan Schmitt
Formalisation de Sémantiques Squelettiques

Les sémantiques squelettiques sont une approche récente pour décrire et manipuler des sémantiques opérationnelles de langages de programmation. Une description squelettique peut être utilisée pour prouver la correction d’une sémantique abstraite ou pour générer un interpréteur en OCaml. Nous décrivons dans ce travail comment automatiquement extraire d’une description squelettique une formalisation en Coq de sa sémantique naturelle. Cette formalisation peut ensuite être utilisée pour prouver des propriétés sur la sémantique, que nous illustrons par la preuve qu’un programme calcule bien la fonction factorielle et par la preuve de correction d’un compilateur d’expressions arithmétiques vers une machine à pile.

Véronique Benzaken , Sarah Cohen-Boulakia , Évelyne Contejean , Rébecca Zucchini et Chantal Keller
Vers une formalisation en Coq de la provenance de données

Dans de multiples domaines scientifiques, de nombreuses données sont générées quotidiennement et doivent être analysées. Dans ces processus d’analyse, les données initiales sont combinées à d’autres jeux de données massifs. Pour garantir une interprétation correcte des résultats de ces analyses de données, il est crucial de pouvoir retracer la provenance des données produites à partir des données initiales. La communauté des bases de données a proposé un cadre formel unifiant de “semi-anneaux de provenance”. L’objectif de cet article est de certifier a posteriori la correction d’une provenance. Pour ce faire, nous proposons une formalisation en Coq fondée sur le modèle de semi-anneaux de provenance pour des analyses de données exprimées en algèbre relationnelle. Nous introduisons ici notamment une preuve d’adéquation de cette provenance avec l’interprétation usuelle de l’algèbre relationnelle. Il s’agit d’une première étape vers la formalisation de langages centrés données avec des garanties fortes de provenance.

Étude formelle de l’implémentation du code des impôts

Le code des impôts définit dans son texte législatif une fonction mathématique permettant de calculer l’impôt sur le revenu d’un foyer fiscal. Afin de recouvrer l’impôt, cette fonction est implémentée sous la forme d’un algorithme par la Direction Générale des Finances Publiques (DGFiP), en utilisant un langage dédié appelé M (pour macro-langage). Nous proposons une sémantique formelle du langage M, testée grâce aux données publiées par la DGFiP. Cette formalisation, couplée à la publication par la DGFiP de la base de code M calculant l’impôt, nous donne accès à une formalisation complète de la portion du code des impôts définissant l’algorithme de calcul de l’impôt sur le revenu. Nous démontrons l’utilité d’une telle formalisation grâce à un prototype à base de solveurs SMT permettant d’inférer des méta-propriétés sur le calcul de l’impôt. Ces méta-propriétés peuvent ensuite compléter et affiner les analyses économiques existantes sur les effets redistributifs de l’impôt sur le revenu, mais aussi de diverses allocations. Plus généralement, une formalisation systématique des portions algorithmiques de la loi permettrait d’augmenter le niveau d’assurance sur la cohérence du système socio-fiscal français. Trois artefacts logiciels accompagnent cet article : une formalisation mécanisée de la sémantique du langage M, un compilateur pour le langage M basé sur cette sémantique, ainsi que le prototype d’encodage du code des impôts dans le solveur SMT Z3.

Articles courts
Martin Desharnais et Stefan Brunthaler
A Generic Framework for Verified Compilers Using Isabelle/HOL’s Locales

The past decade has seen renewed interest in the formal, mechanized verification of compilers, as evidenced by the success of both, CakeML and CompCert. In addition, muttiple smaller compilers or compilation phases get mechanically formalized at an increasing pace. More often than not, these small-scale formalizations lack common abstractions and definitions: they have slightly different ways of encoding the languages’ semantics, compilation functions, how they compose, etc. Time and again, general correctness lemmas — such as forward and backward simulation — need to be defined and proven again and again. Simply put, the idea of reuse has not been adopted on a broader scale. In this article, we present a prototype version of a generic framework for formalizing compiler transformations. Specifically, our framework leverages Isabelle/HOL’s locales to abstract over concrete languages and transformations. The framework thus enables us to state common definitions for language semantics, program behaviours, forward and backward simulations, and compilers. We provide generic operations, such as compiler composition, and prove general theorems, resulting in reusable proof components. By demonstrating our idea on a concrete example, we provide evidence of how locales allow reuse and, therefore, enable encapsulation of verification artifacts into modules.

Antoine Defourné
Better Automation for TLA+ Proofs

TLA+ is a specification language based on traditional untyped set theory. It is equipped with a set of tools, including the TLA+ proof system TLAPS, which uses trusted back-end solvers to handle individual proof steps – referred to as “proof obligations”. As most solvers rely on and benefit from typed formalisms, types are first reconstructed for the obligations; however, the current encoding into the SMTlib format does not exploit all of this type information. In this paper, we present motivations for a more pervasive usage of types at an intermediate representation of TLA + proof obligations, and describe work in progress on several improvements of TLAPS: a type-driven SMT encoding, a tactic for instantiation hints, and type annotations for the language. We conclude with some perspectives for future work.

Frédéric Recoules , Sébastien Bardin , Richard Bonichon , Laurent Mounier et Marie-Laure Potet
Et TInA RUSTInA le lien vers l'assembleur

Le développement en C de logiciels non-critiques utilise régulièrement l’insertion d’assembleur « en ligne », que ce soit pour optimiser certaines opérations ou pour accéder à des primitives systèmes autrement inaccessibles. Celui-ci demande l’écriture de spécifications sous forme de contraintes pour faire le lien entre le langage hôte (C) et le langage assembleur embarqué. Ces spécifications sont ensuite utilisées par le compilateur pour pouvoir insérer l’assembleur dans le code émis, en croyant le programmeur sur parole. Pour éviter les erreurs issues de spécifications mal formées, nous proposons RUSTInA, un outil qui permet de vérifier que les spécifications assembleurs correspondent bien à l’implémentation des blocs qu’elles décrivent, ou, dans le cas contraire diagnostiquer ou corriger le problème.

Loïc Sylvestre et Emmanuel Chailloux
Expérimentations pédagogiques en Learn-OCaml

Learn-OCaml est un logiciel libre destiné à l’enseignement du langage OCaml : il fournit un environnement d’exercices de programmation à correction automatisée. On propose une extension du code source de Learn-OCaml, permettant la séparation et la réutilisation du code de correction et simplifiant l’écriture de tests. Cette extension donne lieu, dans un second temps, à l’élaboration d’une bibliothèque d’aide à la conception d’exercices en Learn-OCaml qui permet de construire des rapports de correction plus adaptés aux constructions avancées du langage. Ces outils ont permis de porter plusieurs séries d’exercices en OCaml utilisées dans des cours de programmation à Sorbonne Université permettant ainsi un premier retour d’expérience positif.

Pierre Chambart , Albin Coquereau et Jacques-Henri Jourdan
Gardez votre mémoire fraiche avec Memthol

Chez OCamlPro, notre usage de OCaml a changé. Là où nous faisions majoritairement des programes terminant, notre modèle d’affaire s’est élargi nous menant à concevoir des systèmes sensés fonctionner pendant de longues durées. Pour ces usages, la manière typique de débogguage de OCaml à grand coup de Printf n’est pas adaptée. En particulier pour les fuites mémoires lentes, difficilement observables hors de la production. Imaginons, au hasard, un serveur maintenant une chaîne-de-blocs qui fuiterait quelques octets par connections. En fonctionnement normal, cela est perdu dans le bruit du glaneur de cellules (GC). Mais un attaquant le découvrant pourrait facilement en profiter pour disrupter le service. Nous proposons une solution intégrée, pour découvrir, analyser et traiter cette problématique sur des logiciels déployés. Un outil d’analyse statistique léger permettant de collecter à un coût modeste et en continu les schémas d’allocations et de désalloctions. Celui ci est couplé à un mechanisme de collecte exaustive du graphe mémoire utilisé quand un problème est identifié. Y est adjoint une interface utilisateur pour cibler l’attention du dévelopeur vers les points clefs et le guider vers la correction.

Mesurer la hauteur d'un arbre

Dans cet article, nous nous intéressons au problème du calcul de la hauteur d’un arbre. Le problème a l’air plutôt simple, à priori,puisqu’il suffit de suivre la définition mathématique avec unesimple fonction récursive de quelques lignes. Néanmoins, une tellefonction peut facilement faire déborder la pile d’appels. Aprèsavoir laissé le lecteur réfléchir à une solution, nous en discutonsplusieurs, notamment au regard de ce qu’offre le langage deprogrammation. Ce problème illustre la difficulté qu’il peut y avoir à se passer de récursivité.

Vincent Semeria
Nombres réels dans Coq

Jusqu’à la version 8.10 de Coq, les nombres réels de la bibliothèque standard étaient axiomatisés, de façon semi-classique. Ceci posait 3 problèmes : la cohérence de ces axiomes n’était pas formellement prouvée (elle était informellement dérivable du modèle ensembliste de Coq étendu avec l’axiome du choix et la logique classique), ces axiomes bloquaient les calculs (la réduction sous forme normale des approximations rationnelles) et enfin l’utilisateur ne pouvait pas se restreindre aux nombres réels constructifs.

Nous présentons une découpe des nombres réels de Coq en une première couche constructive et sans axiome, suivie d’une seconde couche qui donne les nombres réels classiques par quotient de la première couche. L’absence d’axiome dans la couche constructive établit sa cohérence avec le coeur de Coq, c’est-à-dire le calcul des constructions inductives. Elle garantit également la terminaison des calculs, ce qui est conforme aux attentes des mathématiques constructives. La seconde couche classique introduit quelques axiomes, qui sont vrais dans le modèle ensembliste de Coq, leur cohérence est donc prouvée. Enfin l’utilisateur a désormais le choix d’utiliser les nombres réels constructifs ou classiques, selon quels fichiers de la bibliothèque standard il importe.

Cette découpe a été intégrée dans la bibliothèque standard de Coq le 5 août 2019, pour une sortie dans la prochaine version 8.11. Elle est rétro-compatible: toutes les bibliothèques (Coquelicot, Flocq, VST, …) qui utilisaient les nombres réels de Coq jusqu’à la version 8.10 continuent de compiler et de fonctionner, sans aucune modification de leur code source.

Guillaume Baudart , Louis Mandel , Marc Pouzet , Eric Atkinson , Benjamin Sherman et Michael Carbin
Programmation d’applications réactives probabilistes

Les langages synchrones ont été introduits pour la conception de systèmes embarqués temps-réel. Ces langages dédiés permettent de décrire précisément les spécifications du système, et ainsi de le simuler, le tester, le vérifier, et finalement le compiler en du code exécutable. Cependant, ces langages offrent un support limité pour modéliser les comportements non-déterministes qui sont omniprésents dans les systèmes embarqués. ProbZélus est une récente extension probabiliste d’un langage synchrone descendant de Lustre. ProbZélus permet de décrire des modèles probabilistes réactifs, c’est-à-dire, en interaction avec un environnement observable. Lors de l’exécution, un ensemble de techniques d’inférence peut être utilisé pour apprendre les distributions de paramètres latents du modèle à partir de données observées. Dans cet article nous illustrons l’expressivité de ProbZélus avec des exemples comme un détecteur de trajectoire à partir d’observations bruitées, ou un contrôleur de robot capable d’inférer à la fois sa position et une carte de son environnement.

Célestine Sauvage , Reynald Affeldt et David Nowak
Vers la formalisation en Coq des transformateurs de monades modulaires

Nous étudions la vérification formelle de programmes avec effets de bord en utilisant un langage purement fonctionnel. Dans le cadre de cette étude, nous avons développé Monae, une librairie Coq qui propose une formalisation des monades et de leurs lois algébriques. Les preuves se font par raisonnement équationnel en utilisant les capacités de réécriture de Coq. Les programmes n’utilisent généralement pas un seul type d’effet de bord, mais une combinaison de plusieurs d’entre eux. On utilise les transformateurs de monades dans ce but. Cependant, l’approche traditionnelle pour le lifting des primitives n’est pas modulaire. Il est intéressant de définir de manière canonique les opérations algébriques des monades et leurs primitives lift. Dans cet article, nous présentons l’implémentation des transformateurs de monades modulaires et les preuves des théorèmes qui en découlent en Coq. Nous montrons également leurs utilisations comparées aux transformateurs de monades classique.

Appel à soumission

 Les 31es Journées Francophones des Langages Applicatifs (JFLA) se tiendront à Gruissan, plus précisément Hôtel Phoebus Garden & spa , du mercredi 29 janvier 2020 au samedi 1er février 2020 .

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

  • Article de recherche de seize pages au plus (bibliographie incluse), 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 (bibliographie incluse), pour décrire un prototype, faire la démonstration d'un outil, rechercher de l'aide pour résoudre un problème particulier, ou reparler d'un papier déjà publié.

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.

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=jfla20

Organisation

Comité de programme

Zaynah Dargaye Nomadic Labs Présidente
Yann Regis-Gianas IRIF, Université Paris-Diderot Vice-président
Valentin Blot Inria Saclay
Vincent Botbol Nomadic Labs
Emmanuel Chailloux LIP6, Sorbonne Université
Delphine Demange Univ Rennes, Inria, CNRS, IRISA
Chantal Keller LRI, Université Paris-Sud
Marie Kerjean Inria Rennes-Bretagne Atlantique
Alain Mebsout OCamlPro
Julien Narboux ICube, Université de Strasbourg
Marie Pelleau Université de Nice
Pierre-Marie Pédrot Inria Rennes-Bretagne Atlantique
Gabriel Scherer Inria Saclay

Comité de pilotage

Pierre Castéran LaBRI
Catherine Dubois École Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)
Micaela Mayero LIPN, Université Paris 13
Alan Schmitt Inria Rennes - Bretagne Atlantique
Julien Signoles CEA LIST
Pierre Weis Inria Paris

Soutiens

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