Principes de la Vérification de Programmes à Effets Monadiques Arbitraires

Computational monads are a convenient algebraic gadget to uniformlyrepresent side-effects in programming languages, such as mutablestate, divergence, exceptions, or non-determinism. Various frameworksfor specifying programs and proving that they meet their specificationhave been proposed that are specific to a particular combination ofside-effects. For instance, one can use Hoare logic to verify thefunctional correctness of programs with mutable state with respect topre/post-conditions specifications, which are predicates on states.The goal of this thesis is to devise a principled semantic frameworkfor verifying programs with arbitrary monadic effects in a generic waywith respect to such rich specifications. One additional challenge issupporting various interpretations of effects, for instance total vspartial correctness, or angelic vs demonic nondeterminism. Finally,the framework should also accommodate relational verification, forproperties such as program equivalence.Les effets de bord présent dans les languages de programmation tel quel'état mutable, la divergence ou le non déterminisme sont capturés demanière élégante par des monades. Plusieurs systèmes ont été proposéspour spécifier et prouver que des programmes manipulant une certainecombinaison d'effets respectent leur spécification. Par exemple, lalogique de Hoare permet de vérifier la correction de programmesmanipulant la mémoire en stipulant des prédicats sur les étatsinitiaux et finaux. Le but de cette thèse est de définir un cadresémantique générique pour vérifier que des programmes avec des effetsmonadique arbitraire respectent de telles spécifications. Lesinterprétations diverses des effets tel que la correction totale oupartielle, ou encore le non-déterminisme angélique ou démonique,introduisent un défi supplémentaire. Ce cadre sémantique devra aussiconsidérer la vérification de propriétés relationnelles, par exemplela simulation ou l'équivalence de programmes