JFLA 2025

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

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

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

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

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

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

Dans cet exposé, je m’appuyerai sur mon expérience d’enseignement de la programmation fonctionelle en M2 dans un cours, partagé avec mes collègues au sein du MPRI, intitulé “Programmation fonctionnelle et systèmes de types” que nous avons fait évoluer au cours du temps. Ce cours, dense, un peu atypique, est orienté vers la métathéorie des langages de programmation, typage et sémantiques, abordée principalement d’un point de vue syntaxique. J’essaierai d’en tirer quelques leçons et de partager avec vous ce que nous avons plus ou moins bien réussi, et de que ce que l’on pourrait certainement mieux faire.

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

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