Représentations bas niveau de structures de données haut niveau // Low Level Memory Representations of High Level Datastructures

Introduits à l'origine dans les années 80, les types de données algébriques (ADT) sont apparus au cours de la dernière décennie comme un outil incroyablement
efficace pour modéliser et manipuler les données dans le cadre de la programmation. Les types de données algébriques sont la combinaison de « Product types », qui correspondent à des enregistrements, et de « Sum types », qui correspondent à des unions étiquetées, une extension de
énum.

Les types de données algébriques sont également dotés du « pattern matching », une extension de switch qui permet de déconstruire des valeurs complexes de manière pratique et sûre.Dans le cadre du projet Ribbit [3], nous avons développé un langage de spécification pour exprimer une représentation mémoire précise en bits des types de données algébriques [4, 5]. Notre langage de spécification prend en charge une grande variété d'astuces habituellement réalisées
manuellement par les programmeurs, telles que le vol de bits, l'inlining, le unpacking ou même l'unrolling de structures récursives. Ribbit compile ensuite le code de haut niveau écrit par les utilisateurs en une manipulation de la mémoire de bas niveau qui respecte les représentations optimisées de la mémoire.

Jusqu'à présent, Ribbit ne prend en compte que les structures de données composées de types de données algébriques et les manipule de manière pure,
sans effets secondaires. En utilisant notre travail sur Ribbit comme tremplin, l'objectif de ce doctorat sera d'étudier une sémantique plus complexe, qui se rapporte à des structures de données riches et de haut niveau construites avec des types de données algébriques en combinaison avec
d'autres constructions. Cela nous amènera à envisager des schémas d'accès et des algorithmes plus complexes et à les adapter à
représentations de la mémoire spécifiées par l'utilisateur. Par exemple, nous envisagerons les directions suivantes :
- Structures de données mutables et concurrentes
- Types de données algébriques et collections
- Structures de données récursives sans indirection

Traduit avec DeepL.com (version gratuite)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Originally introduced in the 80s, Algebraic Data Types (ADT) have emerged in the last decade as an incredibly effective tool to model and manipulate data for programming. Algebraic Data Types are the combination of “Prod-uct types”, which correspond to records, and “Sum types”, which correspond to tagged unions, an extension oftraditional enumerations. Algebraic Data Types are also provided with “pattern matching”, an extension of switch
which allow to deconstruct complex values conveniently and safely.In the Ribbit [3] project, we have developed a specification language to express bit-precise memory represen-
tation of Algebraic Data Types [4, 5]. Our specification language supports a wide variety of tricks usually done
manually by programmers, such as bit stealing, inlining, unpacking, or even unrolling of recursive structures. Ribbit
then compiles the high-level code written by users to low-level memory manipulation which respects the optimised
memory representations.

So far, Ribbit only considers data-structures composed of algebraic data types and manipulate in a pure fashion,
without side-effects. Using our work on Ribbit as a stepping stone, the goal of this PhD will be to investigate more complex semantics, that pertain to rich, high level datastructure built with Algebraic Data Types in combination with
other constructs. This will lead us to consider more complex access patterns and algorithms and adapt them to user-specified memory representations. For instance, we will consider the following directions:
- Mutable and concurrent data-structures
- Algebraic Data Types and Collections
- Recursive data-structures with no indirection
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025

Concours allocations

Université Grenoble Alpes

217 MSTII - Mathématiques, Sciences et technologies de l'information, Informatique

Appétence en méthodes formelles (typage, sémantique) expérience en langages fonctionnels
Appetence for formal methods st typing ans semantics experience in functional languages (theory and practise)