JFLA 2023

Journées Francophones des Langages Applicatifs
Praz-sur-Arly (Haute-Savoie)
mardi 31 janvier 2023

vendredi 3 février 2023
Praz-sur-Arly avec des Montgolfières (Image © Fabrice Rumillat, Praz-sur-Arly Tourisme. Photo non contractuelle ;-).)

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

Dates importantes

Soumission des résumés 14 octobre 2022 7 octobre 2022
Soumission des articles 21 octobre 2022 14 octobre 2022
Notification aux auteurs 30 novembre 2022 25 novembre 2022
Soumission version finale 21 décembre 2022 14 décembre 2022
Ouverture des inscriptions 19 décembre 2022
Clôture des inscriptions 18 janvier 2023 23 janvier 2023

Inscription

Nous sommes complets ! Les inscriptions sont donc fermées. Contactez-nous si vous souhaitez toujours participer et nous ferons de notre mieux, mais sans garantie malheureusement.

L’Agence VERT COM s’occupe des inscriptions aux JFLA 2023. Il est possible de s’inscrire dans un premier temps et de régler les frais ultérieurement. Pour régler votre inscription, accédez à votre profil de pré-inscription.

Grâce à nos généreux sponsors (voir ci-dessous), l’inscription est gratuite pour les étudiant·es orateur·ices, au lieu de 700€ au tarif normal. Ces frais comprennent l’aller-retour en autocar entre Sallanches et Praz-sur-Arly, le logement en binôme (chambre privative, salle de bain partagée) et les repas.

Transport

L’accès aux JFLA en montagne en hiver est forcément un peu compliqué. Pour accéder à Praz-sur-Arly, nous conseillons la gare de Sallanches.

Nous vous conseillons d’organiser et réserver dès que possible vos transports pour rejoindre Sallanches. Des suggestions de trains pour passer via Paris ou Lyon sont données ci-dessous.

Pour rejoindre le site des JFLA 2023, nous avons réservé un autocar pour l’aller/retour. En dehors de cet autocar réservé, d’autres options sont possibles (voir plus bas).

Aller (31 janvier 2023) vers Sallanches

  • 2e partie (TER) supprimée: 12h43 Paris Gare de Lyon ⇒ 18h24 Sallanches (TGV INOUI N° 6941, TER N° 884119)

  • 06h39 Paris Gare de Lyon ⇒ 14h14 Sallanches (TGV INOUI N°6931, TER, AUTOCAR N°49505)

  • 2e partie (TER) supprimée: 14h38 Lyon Part Dieu ⇒ 18h09 Sallanches (TER N° 96514, TER N° 884525, TER)

  • 09h08 Lyon Part Dieu ⇒ 14h14 Sallanches (TER N° 17974, TER, AUTOCAR N° 49505)

Retour (3 février 2023) depuis Sallanches

  • 14h54 Sallanches ⇒ 19h47 Paris Gare de Lyon (TER N° 884672, LYRIA N° 9786)

  • 14h54 Sallanches ⇒ 19h22 Lyon Part Dieu (TER N° 884672, TER N° 96574)

Aller-retour (autocar) entre Sallanches et Praz-sur-Arly:

Nous organisons un aller/retour en autocar pour les journées.

  • Annecy vers Praz-sur-Arly via Sallanches :

    Départ en gare SNCF d’Annecy, mardi 31 janvier à 18h45. Il s’agit d’un autocar Borini avec affiche « JFLA 2023 ».

  • Sallanches vers Praz-sur-Arly :

    Départ en gare de Sallanches, lundi 30 janvier à 18h45. Il s’agit d’un autocar Borini avec affiche « JFLA 2023 ».

    Le voyage devrait prendre une heure environ.

    Le dîner aura lieu sur site peu après notre arrivée.

    Les exposés ne commenceront que le lendemain matin.

  • Praz-sur-Arly vers Sallanches :

    Départ du site Belambra, vendredi 3 février, après la dernière session d’exposés.

    L’arrivée est prévue pour 14h30 en gare de Sallanches.

Autres transports vers, et au départ de, Praz-sur-Arly:

  • Adresse du site des journées :

    Club Belambra “L’Alisier”

    476 route du Val d’Arly

    74120 Praz-sur-Arly

  • Liaison en car Sallanches - Praz-sur-Arly (17km) : 04 50 21 90 57
  • Taxis :
    • Arvin-Bérod Sébastien : 06 87 80 61 43
    • Alpes Transport : 04 50 55 32 88 / 06 80 03 78 20
  • Informations de l’Office du tourisme de Praz-sur-Arly : voir ici

Programme

Exposés invités

Sylvie Boldo (Inria Saclay)
À propos de l'agrégation d'informatique

Cet exposé présentera l’agrégation externe d’informatique ainsi qu’un retour sur sa première session qui a eu lieu en 2022.

Le rapport du jury sur la session 2022 se trouve à l’adresse suivante.

Plus d’informations (épreuves, annales, environnement informatique, FAQ…) se trouvent sur le site du jury, à l’adresse suivante.

Xavier Leroy (Collège de France)
Théorie et pratique des effets en OCaml 5

La version 5 d’OCaml ajoute, sous forme de bibliothèque, un nouveau trait au langage Caml: les effets définis par l’utilisateur et les gestionnaires d’effets.

La première partie de ce cours illustrera la pratique des effets en OCaml 5. On peut les voir comme une généralisation des exceptions: lever un effet interrompt le calcul en cours, tout comme lever une exception; mais au contraire des exceptions, le calcul en cours peut être redémarré plus tard. C’est le gestionnaire de l’effet qui décide quand et avec quelle valeur redémarrer ce calcul.

Une première utilisation des effets est l’inversion du contrôle, comme par exemple transformer un itérateur fonctionnel «à la Caml» en itérateur générateur «à la Java». Toutes sortes de coroutines peuvent également être définies par l’utilisateur en termes d’effets. Plus généralement, les effets d’OCaml 5 ont la puissance d’expression des continuations délimitées linéaires.

Nous terminerons ce tutoriel en esquissant l’implémentation d’une bibliothèque de fibres (lightweight threads) avec entrées/sorties non bloquantes, utilisables en style direct (pas de passage explicite de continuations comme avec la bibliothèque LWT). La bibliothèque EIO en cours de développement pousse cette approche à base de fibres jusqu’à fournir une alternative performante et en style «direct» à LWT.

Dans la deuxième partie du cours, nous aborderons les fondations théoriques des effets et des gestionnaires d’effets. Nous partirons des monades, un concept issu de la théorie des catégories et appliqué à la sémantique dénotationnelle par Moggi en 1989 puis à la programmation fonctionnelle pure par Wadler et d’autres dès 1991. Les monades fournissent un cadre élégant pour décrire de nombreuses sortes d’effets allant de l’affectation à la programmation probabiliste.

Le lambda-calcul «computationnel» de Moggi décrit de manière indépendante de la monade sous-jacente la propagation des effets. Mais la manière dont les effets sont engendrés et gérés est propre à chaque monade. La théorie des effets algébriques de Plotkin et Power fournit un cadre général pour décrire la génération et le traitement des effets et les spécifier de manière algébrique via des équations, un peu comme dans les types abstraits algébriques. Cette théorie débouche naturellement sur les gestionnaires d’effets comme nouvelle construction du langage permettant d’implémenter les effets algébriques.

Le cours se terminera par une brève discussion du typage statique des effets, qui n’est pas encore implémenté en OCaml 5 mais pour lequel plusieurs systèmes de types ont été proposés, ainsi que de la preuve par vérification déductive de programmes utilisant des effets.

Cours invités

Cyril Cohen (Inria Sophia Antipolis)
Tutoriel Mathematical Components

Mathematical Components est un ensemble de bibliothèques de mathématiques formalisées développées avec l’assistant de preuve Coq. Ces bibliothèques ont été utilisées pour des projets de formalisation à grande échelle, tels que celle du théorème des quatre couleurs et du théorème de l’ordre impair (Feit-Thompson).

Dans ce cours en deux parties, nous explorerons les bibliothèques Mathematical Components disponibles et je fournirai des éléments pour en lire le contenu, les utiliser et y contribuer.

La première partie du cours donnera des clés de lecture de la bibliothèque, et en particulier comment y trouver et utiliser les résultats recherchés. Pour cela nous passerons en revue les conventions de nommage et d’usage en vigueur, afin de faire des recherches pertinentes dans le contenu des bibliothèques. Nous verrons également comment lire les scripts de preuve écrits avec le langage de tactique SSReflect, ainsi que les quelques tactiques indispensables pour utiliser des résultats de la bibliothèque. Cela sera illustré avec quelques exemples lors de session d’exercices encadrés.

La deuxième partie du cours sera consacrée aux hiérarchies de structures présentes dans les bibliothèques Mathematical Components et à la manière dont elles sont générées avec Hierarchy Builder à partir de la version 2.0+alpha1 de Mathematical Components. Je présenterai les motivations pour l’utilisation de Hierarchy Builder par rapport à une gestion manuelle avec des records, des classes ou des modules. Ensuite nous examinerons les différentes façons d’instancier des structures, puis comment ajouter des nouvelles structures en utilisant Hierarchy Builder, et enfin comment modifier du code tout en préservant la compatibilité arrière.

En détail

mardi 31 janvier

  • 18:45 — 19:45
    Autocar de Sallanches à Praz-sur-Arly

mercredi 1er février

  • 08:55 — 09:00
    Ouverture des JFLA 2023
  • 09:00 — 10:00
    Xavier Leroy (Collège de France)
    Théorie et pratique des effets en OCaml 5

    La version 5 d’OCaml ajoute, sous forme de bibliothèque, un nouveau trait au langage Caml: les effets définis par l’utilisateur et les gestionnaires d’effets.

    La première partie de ce cours illustrera la pratique des effets en OCaml 5. On peut les voir comme une généralisation des exceptions: lever un effet interrompt le calcul en cours, tout comme lever une exception; mais au contraire des exceptions, le calcul en cours peut être redémarré plus tard. C’est le gestionnaire de l’effet qui décide quand et avec quelle valeur redémarrer ce calcul.

    Une première utilisation des effets est l’inversion du contrôle, comme par exemple transformer un itérateur fonctionnel «à la Caml» en itérateur générateur «à la Java». Toutes sortes de coroutines peuvent également être définies par l’utilisateur en termes d’effets. Plus généralement, les effets d’OCaml 5 ont la puissance d’expression des continuations délimitées linéaires.

    Nous terminerons ce tutoriel en esquissant l’implémentation d’une bibliothèque de fibres (lightweight threads) avec entrées/sorties non bloquantes, utilisables en style direct (pas de passage explicite de continuations comme avec la bibliothèque LWT). La bibliothèque EIO en cours de développement pousse cette approche à base de fibres jusqu’à fournir une alternative performante et en style «direct» à LWT.

    Dans la deuxième partie du cours, nous aborderons les fondations théoriques des effets et des gestionnaires d’effets. Nous partirons des monades, un concept issu de la théorie des catégories et appliqué à la sémantique dénotationnelle par Moggi en 1989 puis à la programmation fonctionnelle pure par Wadler et d’autres dès 1991. Les monades fournissent un cadre élégant pour décrire de nombreuses sortes d’effets allant de l’affectation à la programmation probabiliste.

    Le lambda-calcul «computationnel» de Moggi décrit de manière indépendante de la monade sous-jacente la propagation des effets. Mais la manière dont les effets sont engendrés et gérés est propre à chaque monade. La théorie des effets algébriques de Plotkin et Power fournit un cadre général pour décrire la génération et le traitement des effets et les spécifier de manière algébrique via des équations, un peu comme dans les types abstraits algébriques. Cette théorie débouche naturellement sur les gestionnaires d’effets comme nouvelle construction du langage permettant d’implémenter les effets algébriques.

    Le cours se terminera par une brève discussion du typage statique des effets, qui n’est pas encore implémenté en OCaml 5 mais pour lequel plusieurs systèmes de types ont été proposés, ainsi que de la preuve par vérification déductive de programmes utilisant des effets.

  • 10:00 — 10:25
    Jean Abou Samra , Martin Bodin et Yannick Zakowski

    Monadic programming is a popular way to embed effectful computations in purely functional languages. In particular, the so-called free-monad comes with the promise of extensibility and modularity: computations are seen as syntax arising from a signature of operations they may perform. Popularized in a programming context, the approach is nowadays used for verification in proof assistants as well, as witnessed by frameworks such as FreeSpec or Interaction Trees.

    In this work in progress, we investigate the following question. Can we type each subcomputation with their minimal valid operation signature, and seamlessly combine all these monadic computations of different natures? Furthermore, can we leverage this additional precision in typing to derive monadic invariants for free?

    We answer positively by suggesting two simple ideas. First, a bind operation between computations living in distinct monads can be defined by transporting them through monad morphisms. Second, to give more structure to the monads we manipulate by indexing them by a semi-lattice as a means to automatically infer the adequate morphisms. We illustrate the benefits on a minimal Coq example: a computation interacting with a memory cell.

  • 11:00 — 11:25
    Théophile Wallez

    TreeSync est un sous-protocole d’authentification pour MLS, un protocole de messagerie de groupe sécurisé en cours de standardisation à l’IETF. Nous formalisons MLS en F∗, et présentons un théorème de sécurité pour TreeSync à l’aide du cadriciel de cryptographie symbolique DY∗. Afin de comprendre les hypothèses clés qui permettent d’exprimer un tel théorème, nous présentons en détail le fonctionnement interne de DY∗. Au cours de notre analyse, nous avons proposé plusieurs changements à TreeSync qui ont été intégrés à MLS, et avons développé de nouvelles méthodes de preuves pour passer à l’échelle avec DY* afin de pouvoir s’attaquer à un gros protocole comme MLS, par exemple, un mécanisme permettant à la fois l’exécution concrète et symbolique du protocole, la génération automatique de parseurs et sérialiseurs binaires vérifiés, ou encore la génération d’invariants globaux du protocole à partir d’invariants locaux.

  • 11:25 — 11:50
    Évelyne Contejean et Andrei Samokish

    Usually, the description of nuclear equipment by the FMEA (Failure Mode and Effects Analysis) method can be of considerable length (up to 5,000 lines); on the other hand, the number of rules used for the verification of this equipment is small. In addition, upstream, there is the question of trust in the tools that generate these descriptions for complex equipment, that is to say, made up of several thousand objects (requirements, functions, interfaces, behaviors).

    Our objective is to formally prove in the Coq proof assistant the accuracy and exhaustiveness of the safety analysis for these nuclear equipments, by proposing a more modular and more abstract framework which is based on an axiomatic description of the systems. - these axioms being either accepted or proven independently of the verification itself. The very nature of the inductive types of Coq is perfectly suited to the description of complex systems, which are systems of systems in interaction. We have a first prototype that demonstrates the feasibility of this approach, for simple properties which are effectively proven by reflection - for example, the study of flows, which must first be produced and then consumed exactly once in the whole system.

    We open the way to a general approach for the proofs of the properties of a (model of) systems and study the kind of properties that can be demonstrated in this way. Finally, we propose the approach for faithful translation of a DSL (domain-specific language) tool into Coq and the proof of its correctness.

  • 11:50 — 12:05
    Jean-Christophe Filliâtre et Andrei Paskevich

    Nous, praticiens de la preuve de programmes, souhaitons que le processus de la vérification soit le plus automatique possible. Les meilleurs outils pour cela sont à l’heure ac- tuelle les démonstrateurs SMT, qui combinent notamment la logique du premier ordre et l’arithmétique linéaire. Par opposition, le raisonnement inductif n’est pas un point fort des démonstrateurs automatiques. Or, les programmes utilisant des pointeurs le font souvent pour manipuler des structures récursives : listes, arbres, etc.

    Dans cet article, nous décrivons une approche qui permet d’amener la preuve de programmes avec pointeurs à la portée des démonstrateurs automatiques. L’idée consiste à projeter une structure récursive sur un domaine numérique, de sorte que les propriétés de possession et de séparation deviennent exprimables en terme de simples inégalités arithmétiques. En plus de simplifier la preuve, cela permet une spécification claire et naturelle. On illustre cette approche avec l’exemple classique du renversement en place d’une liste simplement chaînée.

  • 12:05 — 12:20
    Arthur Correnson

    Les nombres flottants tels que définis dans le standard IEEE-754 sont la solution la plus répandue pour approximer les nombres réels en machine. Toutefois, en pratique, de nombreux environnements logiciels et matériels présentent des subtilités non conformes avec ce standard. Cela complique la tâche de raisonner formellement sur les programmes effectuant des calculs numériques sans connaître a priori leur environnement d’exécution. Dans cet article, nous montrons l’impact de ce problème sur le compilateur CompCert, un compilateur formellement vérifié pour le langage C et proposant un support pour les flottants IEEE-754. Nous présentons les résultats d’un travail d’investigation visant à mesurer les difficultés liées à l’intégration de nouveaux types de flottants dans CompCert. Cette étude est motivée par la volonté d’étendre le compilateur à des cibles non conformes IEEE-754 utilisées, par exemple, en informatique embarquée.

  • 14:00 — 15:30
    Cyril Cohen (Inria Sophia Antipolis)
    Tutoriel Mathematical Components

    Mathematical Components est un ensemble de bibliothèques de mathématiques formalisées développées avec l’assistant de preuve Coq. Ces bibliothèques ont été utilisées pour des projets de formalisation à grande échelle, tels que celle du théorème des quatre couleurs et du théorème de l’ordre impair (Feit-Thompson).

    Dans ce cours en deux parties, nous explorerons les bibliothèques Mathematical Components disponibles et je fournirai des éléments pour en lire le contenu, les utiliser et y contribuer.

    La première partie du cours donnera des clés de lecture de la bibliothèque, et en particulier comment y trouver et utiliser les résultats recherchés. Pour cela nous passerons en revue les conventions de nommage et d’usage en vigueur, afin de faire des recherches pertinentes dans le contenu des bibliothèques. Nous verrons également comment lire les scripts de preuve écrits avec le langage de tactique SSReflect, ainsi que les quelques tactiques indispensables pour utiliser des résultats de la bibliothèque. Cela sera illustré avec quelques exemples lors de session d’exercices encadrés.

    La deuxième partie du cours sera consacrée aux hiérarchies de structures présentes dans les bibliothèques Mathematical Components et à la manière dont elles sont générées avec Hierarchy Builder à partir de la version 2.0+alpha1 de Mathematical Components. Je présenterai les motivations pour l’utilisation de Hierarchy Builder par rapport à une gestion manuelle avec des records, des classes ou des modules. Ensuite nous examinerons les différentes façons d’instancier des structures, puis comment ajouter des nouvelles structures en utilisant Hierarchy Builder, et enfin comment modifier du code tout en préservant la compatibilité arrière.

  • 15:30 — 15:55
    Gabriel Scherer

    François Pottier’s unionFind library is parameterized over an underlying store of mutable references, and provides the usual references, transactional reference stores (for rolling back some changes in case of higher-level errors), and persistent reference stores. We extend this library with a new implementation of backtracking reference stores, to get a UnionFind implementation that efficiently supports arbitrary backtracking and also subsumes the transactional interface.

    Our backtracking reference stores are not specific to unionFind, they can be used to build arbitrary backtracking data structures. The natural implementation, using a journal to record all writes, provides amortized-constant-time operations with a space overhead linear in the number of store updates. A refined implementation reduces the memory overhead to be linear in the number of store cells updated, and gives performance that match non-backtracking references in practice.

  • 15:55 — 16:10
    Denis Carnier , Arthur Correnson , Christopher McNally et Youssef Moawad

    In this presentation, we showcase Goose: an OCaml library to model, simulate and compile low-level quantum programs. Goose is designed as a playground with an emphasis on extensibility and accessibility to non-experts. The library is compatible with the OpenQASM standard, and targets a variety of backends with a minimalistic, circuit-based IR.

  • 16:40 — 17:40
    Sylvie Boldo (Inria Saclay)
    À propos de l'agrégation d'informatique

    Cet exposé présentera l’agrégation externe d’informatique ainsi qu’un retour sur sa première session qui a eu lieu en 2022.

    Le rapport du jury sur la session 2022 se trouve à l’adresse suivante.

    Plus d’informations (épreuves, annales, environnement informatique, FAQ…) se trouvent sur le site du jury, à l’adresse suivante.

  • 17:40 — 18:05
    Amélie Ledein et Elliot Butte

    Ces dernières années, le nombre d’assistants à la preuve, de prouveurs automatiques et de vérificateurs de preuve n’a cessé de croître. L’un d’entre eux, le framework logique Dedukti, a pour objectif de rendre ces outils formels interopérables, c’est-à-dire rendre possible la réutilisation des preuves d’un outil A dans un outil B. Un autre outil formel, Metamath, a la particularité d’être à la 4e place dans la liste des systèmes possédant le plus grand nombre de preuves parmi la liste des 100 théorèmes à prouver de Freek Wiedijk, tout en étant constitué de très peu de fonctionnalités : pas de type dépendant, pas de polymorphisme, ni de notion d’univers. Afin d’agrémenter le nombre de preuves qu’il est possible de traduire dans Dedukti, nous présentons Mathiilde, un traducteur automatique de Metamath vers Dedukti. Comme ce traducteur peut utiliser deux encodages différents de Metamath vers Dedukti, nous discutons les avantages et les inconvénients du point de vue de l’interopérabilité.

  • 18:05 — 18:30
    Guillaume Bertholon et Arthur Charguéraud

    Deductive verification enables one to check that a program satisfies its specification. There are mainly two approaches: either the user provides invariants in the form of annotations and use a tool to extract proof obligations, like in, e.g., Why3; or the user verifies the program through interactive proofs, like in, e.g., CFML, by providing invariants during the proof steps.

    We are interested in expressing in Coq the representation of a program, accompanied with not only its invariants but also its proof terms. Concretely, we present an AST for representing source code and specification in a deep embedding style, and embedded lemmas in shallow embedding style. Such lemmas can be established using the full capabilities of the prover.

    We develop a way to build these ASTs from source code using CFML-style interactive tactics. We also develop a way to build these ASTs by extracting proof obligations from source code already annotated with its invariants. Besides, we provide a way to validate our ASTs by reifying them as Coq proof terms.

    This work is a first step towards a long term project to devise a trustworthy, user-guided, source-to-source optimization framework. On the one hand, we may need to exploit invariants to justify the correctness of code transformations. On the other hand, to be able to chain transformations, we also need every transformation to update the program annotations.

  • 18:30 — 18:40
    Catherine Dubois et Julien Signoles
    Annonces du GDR GPL (Groupement de Recherche Génie de la Programmation et du Logiciel)

    Courte présentation du GDR GPL, et annonce de plusieurs évènements importants. Site web: https://gdr-gpl.cnrs.fr/.

  • 19:00 — 19:30
    Rencontres avec les organismes et entreprises mécènes

jeudi 2 février

  • 09:00 — 10:00
    Sylvie Boldo (Inria Saclay)
    À propos de l'agrégation d'informatique

    Cet exposé présentera l’agrégation externe d’informatique ainsi qu’un retour sur sa première session qui a eu lieu en 2022.

    Le rapport du jury sur la session 2022 se trouve à l’adresse suivante.

    Plus d’informations (épreuves, annales, environnement informatique, FAQ…) se trouvent sur le site du jury, à l’adresse suivante.

  • 10:00 — 10:25
    Clément Blaudeau , Didier Rémy et Gabriel Radanne

    ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remanins difficult to comprehend, requiring heavy machinery to prove their soundness. Building on a previous translation from ML modules to Fω, we propose a new comprehensive description of a generative subset of OCaml modules, embarking on a journey right from the source OCaml module system, up to Fω, and back. We pause in the middle to uncover a system, called canonical that combines the best of both worlds. On the way, we obtain type soundness, but also and more importantly, a deeper insight into the signature avoidance problem, along with ways to improve both the OCaml language and its typechecking algorithm.

  • 10:25 — 10:50
    Samuel Gardelle et Étienne Miquey

    In the realm of the proofs-as-programs correspondence, continuation-passing style (CPS) translations are known to be twofold: they bring both a program translation and a logical translation. In particular, when using the former to compile a language with a control operator, the latter ensures the soundness of the compilation with respect to types.

    This work is inspired by Oliva and Streicher, who explained how Krivine realizability could be rephrased as the composition of a CPS and an intuitionistic realizability model. In this paper, we propose to push one step forward the analysis of the relation between realizability models and CPS translations to investigate the following question: assume that two realizability models are defined using the source and the destination of a CPS translation, is it the case that the CPS translates realizers of a given formula into realizers of the translated formulas?

  • 11:20 — 12:20
    Xavier Leroy (Collège de France)
    Théorie et pratique des effets en OCaml 5

    La version 5 d’OCaml ajoute, sous forme de bibliothèque, un nouveau trait au langage Caml: les effets définis par l’utilisateur et les gestionnaires d’effets.

    La première partie de ce cours illustrera la pratique des effets en OCaml 5. On peut les voir comme une généralisation des exceptions: lever un effet interrompt le calcul en cours, tout comme lever une exception; mais au contraire des exceptions, le calcul en cours peut être redémarré plus tard. C’est le gestionnaire de l’effet qui décide quand et avec quelle valeur redémarrer ce calcul.

    Une première utilisation des effets est l’inversion du contrôle, comme par exemple transformer un itérateur fonctionnel «à la Caml» en itérateur générateur «à la Java». Toutes sortes de coroutines peuvent également être définies par l’utilisateur en termes d’effets. Plus généralement, les effets d’OCaml 5 ont la puissance d’expression des continuations délimitées linéaires.

    Nous terminerons ce tutoriel en esquissant l’implémentation d’une bibliothèque de fibres (lightweight threads) avec entrées/sorties non bloquantes, utilisables en style direct (pas de passage explicite de continuations comme avec la bibliothèque LWT). La bibliothèque EIO en cours de développement pousse cette approche à base de fibres jusqu’à fournir une alternative performante et en style «direct» à LWT.

    Dans la deuxième partie du cours, nous aborderons les fondations théoriques des effets et des gestionnaires d’effets. Nous partirons des monades, un concept issu de la théorie des catégories et appliqué à la sémantique dénotationnelle par Moggi en 1989 puis à la programmation fonctionnelle pure par Wadler et d’autres dès 1991. Les monades fournissent un cadre élégant pour décrire de nombreuses sortes d’effets allant de l’affectation à la programmation probabiliste.

    Le lambda-calcul «computationnel» de Moggi décrit de manière indépendante de la monade sous-jacente la propagation des effets. Mais la manière dont les effets sont engendrés et gérés est propre à chaque monade. La théorie des effets algébriques de Plotkin et Power fournit un cadre général pour décrire la génération et le traitement des effets et les spécifier de manière algébrique via des équations, un peu comme dans les types abstraits algébriques. Cette théorie débouche naturellement sur les gestionnaires d’effets comme nouvelle construction du langage permettant d’implémenter les effets algébriques.

    Le cours se terminera par une brève discussion du typage statique des effets, qui n’est pas encore implémenté en OCaml 5 mais pour lequel plusieurs systèmes de types ont été proposés, ainsi que de la preuve par vérification déductive de programmes utilisant des effets.

  • 17:00 — 18:30
    Cyril Cohen (Inria Sophia Antipolis)
    Tutoriel Mathematical Components

    Mathematical Components est un ensemble de bibliothèques de mathématiques formalisées développées avec l’assistant de preuve Coq. Ces bibliothèques ont été utilisées pour des projets de formalisation à grande échelle, tels que celle du théorème des quatre couleurs et du théorème de l’ordre impair (Feit-Thompson).

    Dans ce cours en deux parties, nous explorerons les bibliothèques Mathematical Components disponibles et je fournirai des éléments pour en lire le contenu, les utiliser et y contribuer.

    La première partie du cours donnera des clés de lecture de la bibliothèque, et en particulier comment y trouver et utiliser les résultats recherchés. Pour cela nous passerons en revue les conventions de nommage et d’usage en vigueur, afin de faire des recherches pertinentes dans le contenu des bibliothèques. Nous verrons également comment lire les scripts de preuve écrits avec le langage de tactique SSReflect, ainsi que les quelques tactiques indispensables pour utiliser des résultats de la bibliothèque. Cela sera illustré avec quelques exemples lors de session d’exercices encadrés.

    La deuxième partie du cours sera consacrée aux hiérarchies de structures présentes dans les bibliothèques Mathematical Components et à la manière dont elles sont générées avec Hierarchy Builder à partir de la version 2.0+alpha1 de Mathematical Components. Je présenterai les motivations pour l’utilisation de Hierarchy Builder par rapport à une gestion manuelle avec des records, des classes ou des modules. Ensuite nous examinerons les différentes façons d’instancier des structures, puis comment ajouter des nouvelles structures en utilisant Hierarchy Builder, et enfin comment modifier du code tout en préservant la compatibilité arrière.

  • 18:30 — 18:45
    Julien Girard-Satabin , Michele Alberti , François Bobot et Zakaria Chihani

    Nous proposons de faire la démonstration de CAISAR, un logiciel libre en développement au sein du laboratoire de sûreté et sécurité des logiciels du CEA LIST. CAISAR est une plateforme permettant de caractériser la sûreté des logiciels résultant d’un protocole d’apprentissage (réseaux de neurones, machines à vecteur de support, forêts aléatoires). CAISAR se base sur la plateforme de vérification Why3 pour fournir un langage typé de modélisation de problèmes, ainsi qu’un moteur de raisonnement logique éprouvé. Cette approche autorise par exemple la vérification de systèmes composés de plusieurs blocs d’IA, ainsi qu’une meilleure expressivité des propriétés à vérifier. CAISAR est disponible à https://git.frama-c.com/pub/caisar.

vendredi 3 février

  • 09:15 — 09:40
    Milla Valnet , Raphaël Monat et Antoine Miné

    Afin de prévenir les erreurs de programmation, des analyseurs statiques ont été développés pour de nombreux langages; cependant, aucun analyseur mature ne cible l’analyse de valeurs pour un langage fonctionnel à la ML. Des outils de vérification pour ces langages existent, tels les systèmes de types classiques ou les méthodes déductives, mais le raisonnement automatique sur des programmes numériques a jusqu’alors été peu exploré. Cet article décrit un analyseur statique de valeurs par interprétation abstraite pour un langage fonctionnel typé du premier ordre, approche sûre et automatique pour garantir l’absence d’erreurs à l’exécution. En se basant sur des domaines abstraits relationnels et en réalisant des résumés des champs récursifs des types algébriques, cette approche permet d’analyser des fonctions récursives manipulant des types algébriques récursifs et d’inférer dans un domaine abstrait leur relation entrée-sortie. Une implémentation est en cours sur la plateforme d’analyse multilangage MOPSA et analyse avec succès de courts programmes de quelques lignes. Ce travail ouvre ainsi la voie vers une analyse de valeurs précise et relationnelle basée sur l’interprétation abstraite pour les langages fonctionnels d’ordre supérieur à la ML.

  • 09:40 — 09:55
    Louis Noizet et Alan Schmitt

    On présente Necro ML, un outil pour générer des interpréteurs OCaml à partir de sémantiques en Skel, un langage minimaliste de description de sémantiques. Ces interpréteurs sont modulaires, en exploitant des monades pour interpréter les calculs.

  • 09:55 — 10:20
    Thomas Jensen , Vincent Rébiscoul et Alan Schmitt

    This paper describes a method to define a correct abstract interpretation from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics. We extend it with a notion of program points, in order to differentiate two fragments of the program that are syntactically equivalent but appear at different locations. We introduce a methodology for deriving an abstract interpretation from a Skeletal Semantics that is correct by construction: given a program, abstract states are computed for each program points. We apply our method by defining a Control Flow Analysis for λ-calculus from its Skeletal Semantics.

  • 10:50 — 11:15
    Guillaume Baudart , Grégoire Bussone , Louis Mandel et Christine Tasson

    ProbZelus étend le langage synchrone Zelus pour permettre de décrire des modèles probabilistes synchrones. Là où la programmation synchrone implémente des fonctions de suites, un langage probabiliste synchrone permet de décrire des modèles qui calculent des suites de distributions. On peut par exemple estimer la position d’un objet en mouvement à partir d’observations bruitées ou estimer l’incertitude d’un capteur à partir d’une suite d’observations. Ces problèmes mêlent des flots de variables aléatoires – les paramètres d’état qui changent au cours du temps – et des variables aléatoires constantes – les paramètres constants.

    Pour estimer les paramètres d’état, les algorithmes d’inférence bayésienne de Monte Carlo séquentiels reposent sur des techniques de filtrage. Le filtrage est une méthode approchée qui consiste à perdre volontairement de l’information sur l’approximation actuelle pour recentrer les estimations futures autour de l’information la plus significative. Malheureusement, cette perte d’information est dommageable pour l’estimation des paramètres constants qui n’évoluent pas au cours du temps. Ce phénomène s’appelle l’appauvrissement.

    Inspirés de la méthode d’inférence Assumed Parameter Filter (APF), nous proposons (1) une analyse statique, (2) une passe de compilation et (3) une nouvelle méthode d’inférence modulaire pour ProbZelus qui évite l’appauvrissement pour les paramètres constants tout en gardant les performances des algorithmes de Monte Carlo séquentiels pour les paramètres d’états.

  • 11:15 — 11:40
    Timothy Bourke , Basile Pesin et Marc Pouzet

    Vélus est une formalisation d’un langage synchrone à flots de données et de sa compilation dans l’assistant de preuve Coq. Il inclut une définition de la sémantique dynamique du langage, un compilateur produisant du code impératif, et une preuve de bout en bout que le compilateur préserve la sémantique des programmes.

    Dans cet article, on spécifie dans Vélus la sémantique de deux structures d’activation présentes dans les compilateurs modernes : switch et déclarations locales. Ces nouvelles constructions nécessitent une adaptation de l’analyse statique de dépendance de Vélus, qui produit un graphe acyclique comme témoin de la bonne formation d’un programme. On utilise ce témoin pour construire un schéma d’induction propre aux programmes bien formés. Ce schéma permet de démontrer le déterminisme du modèle sémantique dans Coq.

  • 11:40 — 11:50
    Clôture des JFLA 2023

Organisation

Comité de programme

Timothy Bourke Inria, ÉNS de Paris, Paris Président
Delphine Demange Univ Rennes, Inria, CNRS, IRISA Vice-présidente
François Bobot CEA LIST, Paris
Lélio Brun National Institute of Informatics, Tokyo
Raphaëlle Crubillé CNRS, LIS, Aix-Marseille
Pierre-Évariste Dagand CNRS, IRIF, Paris
Stefania Gabriela Dumbrava Institut Polytechnique de Paris / ENSIIE, Paris
Benjamin Farinier Université Rennes 1 / IRISA, Rennes
Aymeric Fromherz Inria de Paris, Paris
Diane Gallois-Wong Nomadic Labs, Paris
Assia Mahboubi Inria U. de Rennes, Nantes
Gabriel Radanne LIP ENS Lyon / Inria U. GA, Lyon
Laurence Rideau Inria U. Côte d'Azur, Sophia Antipolis
Pierre Roux Onera, Toulouse
Boris Yakobowski AdaCore, Paris

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 !