Maico Leperle soutiendra sa thèse intitulée Une dissection de l’appel-par-nécessité par la personnalisation des systèmes de multi types le vendredi 7 mai à 16h00. La présentation sera accessible sur la plateforme Zoom via le lien suivant: https://us02web.zoom.us/j/89194059278?pwd=ZVVHcSthMlJiZXpXNDBvZkx1TFNRdz09

Le jury sera composé de :

Rapporteurs :

• Damiano MAZZA, CNRS, France
• Simona RONCHI DELLA ROCCA, Università di Torino, Italie

Examinateurs :

• Eduardo Augusto BONELLI, Stevens Institute of Technology, États-Unis
• Hugo HERBELIN, Université de Paris, France
• Delia KESNER, Université de Paris, France

PhD Advisors

• Advisor: Dale MILLER, INRIA et l’École Polytechnique, France
• Co-advisor: Beniamino ACCATTOLI, INRIA et l’École Polytechnique, France

Résumé: Dans cette thèse, on présente une étude quantitative du lambda calcul en appel-par-nécessité, du côté de la théorie de types ainsi que de celui de la sémantique opérationnelle.

En ce qui concerne la théorie de types, on dérive plusieurs systèmes de multi types—un variant non-idempotent des types d’intersection. Chacun de ces systèmes cible une certaine notion de l’appel-par-nécessité, de telle façon que le typage équivaut à la normalisation dans la version correspondante de l’appel-par-nécessité. Dans chaque cas, la caractérisation de la normalisation est tellement raffinée que l’on est capable d’extraire d’informations quantitatives concernant plusieurs aspects du processus de normalisation—typiquement, le nombre de pas de réduction vers la forme normale et la taille de la forme normale.

En ce qui concerne la sémantique opérationnelle, on suit une approche incrémentale, en partant de la version faible et fermée de l’appel-par-nécessité, formalisée dans un calcul avec des substitutions explicites. En visant le cas le plus général, on l’étend vers le cadre de la réduction faible et ouverte—où les termes sont potentiellement ouverts mais la réduction reste faible—et on appelle cette stratégie l’Open CbNeed. Enfin, on obtient un variant utile de l’Open CbNeed, appelé Useful Open CbNeed.

L’intérêt pour ce variant utile de l’appel-par-nécessité provient de la théorie de la complexité du lambda calcul. En effet, on sait que la preuve de l’existence d’un modèle de coût de temps raisonnable pour le lambda calcul fort—où la réduction peut aller au-dessous des abstractions lambdas—requiert la mise en œuvre des substitutions dites utiles. Ces dernières consistent à réduire les expressions jusqu’à l’obtention d’une forme normale partagée, tandis que l’on n’effectue pas les substitutions ne contribuant pas à son obtention.

La littérature ne contient d’analyses sur les substitutions utiles que pour la stratégie d’évaluation leftmost-outermost, la stratégie d’évaluation standard du lambda calcul, appartenant à la famille de l’appel-par-nom. La présentation de l’Useful Open CbNeed est donc la toute première analyse des substitutions utiles pour l’appel-par-nécessité dans le cadre du lambda calcul fort. Présentées comme un élément clé dans la sémantique opérationnelle de l’Useful Open CbNeed, les substitutions utiles sont ensuite représentées dans le système de multi types de l’Useful Open CbNeed.

Finalement, on dérive une stratégie d’évaluation pour le lambda calcul fort en appel-par-valeur, et puis on étend les résultats quantitatifs du cadre fort du lambda calcul en dérivant un système de multi types pour cette stratégie de l’appel-par-valeur. Ceci concerne la théorie quantitative de l’appel-par-nécessité en tant qu’il est un pas nécessaire pour la mise en œuvre d’un variant fort de l’Useful Open CbNeed, ainsi que d’un système de multi types le caractérisant et ayant les propriétés quantitatives désirées.