JFLA 2026

On dit souvent que le lambda-calcul est le fondement théorique de la programmation fonctionnelle. On en déduit parfois que, le lambda-calcul étant Turing-complet, nos langages applicatifs favoris le sont également. On remarque plus rarement que les codages permettant habituellement de justifier la complétude du lambda-calcul s’accommodent mal d’un cadre de programmation fonctionnelle ordinaire, et en particulier cohabitent difficilement avec le typage.

Je vous propose une courte présentation de FaustML : un mini-fragment d’OCaml à visée pédagogique, qui offre une manière d’aborder la théorie de la calculabilité tout en restant dans le cadre ordinaire de la programmation applicative, statiquement et élémentairement typée.

Sek est une structure de données “transiente” implémentée en OCaml, permettant d’implémenter des séquences et notamment des piles, des files, ou des tableaux. Le principe des structures transientes est de combiner les avantages des structures persistentes avec ceux des structures éphémères. D’une part, une structure transiente peut s’utiliser comme une structure persistente, dont on peut conserver des copies de toutes les versions et notamment prendre des snapshots. D’autre part, une structure transiente peut être temporairement convertie en une structure éphémère permettant d’effectuer, dans les cas favorables, la plupart des mutations “en place”. Ce court exposé vise à présenter l’API du paquet opam Sek, afin de faire connaître non seulement cette structure de données particulière, mais également de mettre en avant le potentiel des structures transientes. L’exposé inclura aussi des résultats de micro-benchmarks.

On a développé Topiary initialement en essayant de faire un formateur pour Nickel. Écrire un (bon) formateur de code est aujourd’hui considéré comme une base du tooling pour un langage, mais c’est étonnamment fastidieux et non-trivial. Il n’y a surtout (à ma connaissance en tout cas) aucun outil ou framework spécifique pour nous aider, contrairement par exemple au parsing avec des générateurs de parsers à la Menhir. On doit l’écrire à la main.

L’idée de Topiary est de réutiliser l’infrastructure existante de tree-sitter, une librairie de parsing incrémental et un écosystème de grammaires (très utilisé dans les éditeurs typiquement), pour permettre d’écrire des formateurs de manière déclarative. Concrètement, on écrit une grammaire tree-sitter pour son langage, et des queries tree-sitter qui sont en gros des patterns qui attachent des directives de formatting aux nœuds de l’AST correspondants. Topiary utilise ces query pour ensuite formater des fichiers sources.

Comme pour Menhir par exemple, l’idée est de se concentrer sur la structure et de laisser l’outil gérer le reste (I/O, parsing, pretty-printing). Pour plus de détails, j’ai écrit un post d’introduction. Je sais que l’équipe de Kadena l’utilise comme formateur officiel, Nickel aussi évidemment, il y a d’autres langages plus niches (je crois que Nushell étudient aussi l’idée, Il y a GDScript, etc), et Topiary supporte OCaml à un niveau qui en fait une alternative sérieuse à OcamlFormat.

D’après un utilisateur (dans le README de GDScript): Since Scony made his great formatter, new technologies have come up that could make it much easier to build and maintain one: Tree Sitter and Topiary. This project started as a suggestion from one of Godot’s core contributors to test these new technologies for GDScript formatting. While testing it, I could get results within just a couple of hours and found it to be a very promising approach that could lead to a simple and fast formatter that’s relatively easy to maintain and extend for the community.

Suite à votre appel à présentations courtes d’artefacts logiciels pour les JFLA, je souhaiterais vous proposer une présentation du prototype CAVOC : https://github.com/g-jaber/cavoc-proto

CAVOC implémente une sémantique interactive – plus précisément une sémantique des jeux opérationnelle – pour un large fragment d’OCaml, incluant l’ordre supérieur, les références mutables, le polymorphisme, les types abstraits, et les exceptions.

Concrètement, l’outil prend en entrée le code OCaml d’un module ainsi que sa signature, puis permet à l’utilisateur de jouer le rôle d’un client de ce module, en interagissant avec ses fonctions conformément à l’interface spécifiée par la signature.

Le prototype implémente une partie du “cube sémantique”, offrant la possibilité de contraindre l’interaction afin de respecter (ou non) les conditions de bon parenthésage et de visibilité, correspondant respectivement à l’absence d’opérateurs de contrôle et de références d’ordre supérieur.

CAVOC est accompagné d’un frontend web, qui permet notamment de visualiser l’état courant du jeu après une succession d’interactions (appels de fonctions et retours), et de choisir la prochaine interaction à effectuer. Ce frontend a été réalisé par des étudiants du parcours Architectures logicielles du Master informatique de Nantes Université, dans le cadre d’un projet que j’ai encadré ces deux dernières années.

Enfin, un court tutoriel est en cours de réalisation, de difficulté progressive, proposant des exemples de modules munis d’assertions vérifiant des invariants, l’objectif étant pour le joueur de trouver une interaction permettant de rompre ces invariants.

Pattern matching has been around for decades, and subject to extensive research and extensions over the years. Nevertheless, recent features such as Rust’s if-let construct, and recent articles such as Cheng and Parreaux (OOPSLA’24), suggest that there might still be room for improvement. We propose a streamlined presentation that unifies the various constructs related to pattern matching and to extended forms of conditionals.

In particular, our prototype features bindings-boolean-expressions, which enable to bind variables in the when-clauses of patterns, to bind variables in a if-condition and use them in the then-branch, and to bind variables in while-conditions and use them in the loop body. Our prototype also features Haskell’s style views, allowing in particular to implement smart-deconstructors, which are the inverse of smart-constructors.

We have presented at the ML workshop the corresponding evaluation rules, typing rules, as well as a naive compilation scheme. In this talk, we will give a demo of our implementation, which takes the form of a prototype that parses an extended ML syntax exposing all our constructs, then performs typechecking according to our (highly intuitive!) rules, and finally produces executable OCaml code via our (non-optimizing) translation.

PS: it is not yet clear whether we will succeed in packaging our prototype into a PPX-package by the time of the JFLA, but we’ll try!