Managing Logical and Computational Complexity using Program Transformations

L'appréhension de la complexité logique en mathématique offre unelongue tradition de mise en place de modèles pour des logiquescomplexes obtenus par extension de modèles pour des logiques plussimples, comme c'est le cas pour la construction de faisceaux. Eninformatique, cette démarche a un pendant dual qui consiste à donnerdu sens à des langages complexes via une phase de compilation vers deslangages plus simples.Dans ce manuscrit, nous montrons en quoi l'approche par compilationfait aussi sens en logique, via l'isomorphisme de Curry-Howard, et esten fait plus précise que l'approche par extension de modèle car elleprend en compte le calcul. Pour illustrer ce propos, nous donnons desexemples de transformation de programmes en théorie des types, avecune application à l'assistant de preuve Coq, et dans une moindremesure en programmation distribuée.