Proof of Programs with Effect Handlers

Preuves de Programmes avec Effect Handlers Cette thèse s'intéresse à la conception de méthodes formelles pour raisonner sur les programmes impératifs qui peuvent modifier le flot de contrôle à travers les gestionnaires d'effets, une nouvelle primitive de programmation offrant une interface relativement simple aux opérateurs de contrôle délimité. Les gestionnaires d'effets sont extrêmement puissants en tant qu'outil de programmation: plusieurs primitives et modes de programmation -- comme la programmation asynchrone -- souvent considérés dans les langages traditionnels comme des parties intégrées de ces langages peuvent être implémentés à l'aide des gestionnaires d'effets. La réputation des gestionnaires d'effets en tant que concept de programmation puissant et modulaire est attestée par le développement du langage OCaml, qui offrira les gestionnaires d'effets dans sa prochaine version majeure. Cet événement fait de la recherche des principes logiques qui sous-tendent les gestionnaires d'effets un problème encore plus pressant. En particulier, comment peut-on raisonner à propos d'une continuation de façon abstraite plutôt que de façon concrète comme un morceau de la pile d'exécution? Comment peut-on raisonner à propos d'un programme qui lance des effets séparément du programme qui attrape ces effets? Cette thèse répond à ces questions en introduisant Hazel, une Logique de Séparation pour les gestionnaires d'effets. Hazel introduit un nouveau langage de spécification permettant la description du comportement des programmes, y compris des continuations. Cette logique permet aussi la composition des spécifications de façon modulaire, soit par l'application de règles de raisonnement habituelles, tel que la règle de liaison ou la règle de l'encadrement; soit par l'application de règles nouvelles, comme les règles pour lancer ou capturer des effets. Pour évaluer l'applicabilité de Hazel en tant qu'outil pour le raisonnement formel sur les programmes, cette thèse inclut la vérification de nombreux cas d'études: (1) la conversion générique d'une méthode d'itération d'ordre supérieur en une séquence paresseuse; (2) une bibliothèque pour la programmation asynchrone; (3) une bibliothèque pour la différentiation automatique en arrière. Cette thèse étudie aussi des variantes de Hazel pour les différentes conceptions de gestionnaires d'effets. Parmi ces variantes se trouve Maze, une logique pour les gestionnaires d'effets avec des continuations à plusieurs appels (multi-shot). L'applicabilité de Maze est évaluée par (1) la vérification d'un solveur SAT simple qui utilise des continuations pour implémenter le rebroussement et par (2) la conception de règles de raisonnement pour call/cc et throw. Une autre variante est TesLogic, une logique pour raisonner sur la génération dynamique de noms d'effets. La principale application de TesLogic est l'étude des systèmes de types pour les gestionnaires d'effets. La conception d'un système de types pour les gestionnaires d'effets est le sujet d'un débat actif: pour offrir des règles simples et permissives de sous-typage, un côté soutient la restriction des gestionnaires d'effets aux gestionnaires d'effets de portée lexicale, tandis que l'autre côté soutient l'adoption de coercions d'effets. Cette thèse contribue à ce débat en introduisant Tes, un système de types qui (1) n'est pas restreint aux gestionnaires d'effets de portée lexicale, (2) n'introduit pas de coercions d'effets, et (3) admet des règles de sous-typage puissantes. La sûreté de Tes est prouvée à l'aide d'une interprétation des jugements de typage en tant que spécifications écrites en TesLogic. Les résultats de cette thèse sont formalisés dans l'assistant de preuve Coq.