9h45

Soutenance de thèse de THOMAS BAGREL

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

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

Jury

Directeur de these_CIRSTEA_Horatiu_Université de Lorraine
Co-encadrant de these_SPIWACK_Arnaud_EURL Tweag
Examinateur_KESNER_Delia_Université Paris Cité
Rapporteur_ORCHARD_Dominic_ University of Kent
Rapporteur_KELLER_Gabriele_Utrecht University
Président_VIGNERON_Laurent_Université de Lorraine
Examinateur_SCHERER_Gabriel_Inria Saclay

école doctorale

IAEM - INFORMATIQUE - AUTOMATIQUE - ELECTRONIQUE - ELECTROTECHNIQUE - MATHEMATIQUES

Laboratoire

LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications

Mention de diplôme

Informatique
A008 LORIA LORIA, bâtiment Ada Lovelace, Campus Scientifique, 615 Rue du Jardin-Botanique, 54506 Vandœuvre-lès-Nancy
*

Mots clés

Passage de destinations,Programmation fonctionnelle,Gestion de la mémoire,Systèmes de types linéaires,Haskell,Coq,

Résumé de la thèse

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.

Keywords

Destination passing,Functional programming,Memory management,Linear type systems,Haskell,Coq,

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.