Thomas BAGREL (Veridis), défendra sa thèse intitulée

Formalisation et implémentation de techniques sûres pour la programmation par passage de destination dans les contextes fonctionnels purs.

La soutenance se déroulera en anglais le vendredi 14 novembre 2025 à 9h45 au Loria, en salle A008. Elle sera suivie d’un pot dans le hall B du Loria.

Jury :

• Dominic Orchard, University of Kent (rapporteur)
• Gabriele Keller, Utrecht University (rapporteuse)
• Delia Kesner, IRIF/Université Paris Cité (examinatrice)
• Laurent Vigneron, LORIA/Université de Lorraine (examinateur)
• Gabriel Scherer, IRIF/Université Paris Cité (examinateur)
• Horatiu Cirstea, LORIA/Université de Lorraine (directeur de thèse)
• Arnaud Spiwack, Tweag (encadrant industriel)

Résumé :

La programmation par passage de destination introduit le concept de destination, qui représente l’adresse d’une cellule mémoire encore vierge sur laquelle on ne peut écrire qu’une fois. Ces destinations peuvent être passées en tant que paramètres de fonction, permettant à l’appelant de garder le contrôle de la gestion mémoire : la fonction appelée se contente de remplir la cellule au lieu d’allouer de l’espace pour une valeur de retour. Bien que principalement utilisé en programmation système, le passage de destination trouve aussi des applications en programmation fonctionnelle pure, où il permet d’écrire des programmes auparavant inexpressibles avec les structures de données immuables usuelles.

Dans cette thèse, nous développons un λ-calcul avec destinations, λd. Ce nouveau système théorique est plus expressif que les travaux similaires existants, le passage de destination y étant conçu pour être aussi flexible que possible. Cette expressivité est rendue possible par un système de types modaux combinant types linéaires et un système d’âges pour gérer le contrôle lexical des ressources, afin de garantir la sûreté du passage de destination. Nous avons prouvé la sûreté de notre système via les théorèmes habituels de progression et de préservation des types, de façon mécanisée, avec l’assistant de preuve Rocq.

Nous montrons ensuite comment le passage de destination, formalisé dans ce calcul théorique, peut être intégré à un langage fonctionnel pur existant, Haskell, dont le système de types est moins puissant que notre système théorique. Préserver la sûreté nécessite alors de restreindre la flexibilité dans la gestion des destinations. Nous affinons par la suite l’implémentation pour retrouver une grande partie de cette flexibilité, au prix d’une complexité accrue pour l’utilisateur.

L’implémentation prototype en Haskell montre des résultats encourageants pour l’adoption du passage de destination pour des parcours ou du mapping de grandes structures de données, telles que les listes ou les arbres.

Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings.

The defense will be held in English on Friday, November 14th, 2025 at 9:45 A.M. at LORIA, in room A008. The defense will be followed by a pot de thèse in the hall B of LORIA

Jury:

• Dominic Orchard, University of Kent (reviewer)
• Gabriele Keller, Utrecht University (reviewer)
• Delia Kesner, IRIF/Université Paris Cité (examiner)
• Laurent Vigneron, LORIA/Université de Lorraine (examiner)
• Gabriel Scherer, IRIF/Université Paris Cité (examiner)
• Horatiu Cirstea, LORIA/Université de Lorraine (PhD supervisor)
• Arnaud Spiwack, Tweag (industrial supervisor)

Abstract:

Destination-passing style programming introduces destinations, which represent the address of a write-once memory cell. These destinations can be passed as function parameters, allowing the caller to control memory management: the callee simply fills the cell instead of allocating space for a return value. While typically used in systems programming, destination passing also has applications in pure functional programming, where it enables programs that were previously unexpressible using usual immutable data structures.

In this thesis, we develop a core λ-calculus with destinations, λd. Our new calculus is more expressive than similar existing systems, with destination passing designed to be as flexible as possible. This is achieved through a modal type system combining linear types with a system of ages to manage scopes, in order to make destination-passing safe. Type safety of our core calculus was proved formally with the Rocq proof assistant.

Then, we see how this core calculus can be adapted into an existing pure functional language, Haskell, whose type system is less powerful than our custom theoretical one. Retaining safety comes at the cost of removing some flexibility in the handling of destinations. We later refine the implementation to recover much of this flexibility, at the cost of increased user complexity.

The prototype implementation in Haskell shows encouraging results for adopting destination-passing style programming when traversing or mapping over large data structures such as lists or data trees.