Combinaisons de théories calculatoires

Les vérificateurs et assistants de preuve sont utilisés pour formaliser des théorèmes mathématiques et la vérification logicielle, notamment de systèmes critiques tels que des sytèmes médicaux, industriels ou de transport. La diversité des systèmes de preuves soulève la question de leur interopérabilité : comment revérifier ou réutiliser des preuves d'un système dans un autre ? Des cadres logiques tels que le lambdaPi-calcul modulo théorie procurent un formalisme commun dans lequel peuvent être exprimées divers systèmes logiques et théories mathématiques. Des outils de transformation de preuves au sein du lambdaPi-calcul modulo théorie permettent alors de traduire des preuves d'un système logique à l'autre.De manière analogue aux cadres logiques, des théories combinant plusieurs théories fournissent un langage commun entre ces théories. L'enjeu principal de ce manuscrit est l'étude de la définition et des propriétés de ces théories, spécifiquement dans le cadre des théories calculatoires, c'est-à-dire dont la définition repose sur la réécriture. Plus précisément, les combinaisons de théories calculatoires seront étudiées dans deux contextes : les logiques œcuméniques, c'est-à-dire des logiques combinant logiques intuitionnistes et classiques, et les théories des systèmes de types purs modulo réécriture, qui sont utilisées dans le lambdaPi-calcul modulo pour exprimer les systèmes logiques de divers assistants de preuve.Dans un premier temps, on s'intéresse au cas particulier des logiques œcuméniques. Une nouvelle logique œcuménique NE est définie et étudiée. Ces principales propriétés sont que sa définition, bien que guidée par, ne repose pas sur les traductions par doubles négations et qu'elle permet la définition de théories œcuméniques calculatoires, par exemple la définition d'une théorie des types simples œcuménique.Dans un second temps, les théories des systèmes de types purs modulo théorie, dont un exemple est le cadre logique du lambdaPi-calcul modulo théorie, sont étudiées. Notamment, des outils permettant de prouver le bon typage de théories calculatoires de manière modulaire sont exhibés, que ce soit pour l'extension ou la restriction (appelée fragmentation) des théories. Finalement, il est établi qu'étant donné une preuve dans une théorie combinant de multiples fragments, il est possible d'établir à quel fragment cette preuve appartient à partir des constantes qu'elle contient, sans indication explicite des règles de réécriture utilisées. Ce résultat est crucial pour justifier l'utilisation de telles théories pour l'interopérabilité des systèmes de preuves.Enfin, en s'appuyant sur la définition deec et sur les résultats de modularité précédents, on s'intéresse à une théorie calculatoire du lambdaPi-calcul nommée théorie U et combinant logiques du premier ordre et d'ordre supérieur minimales, intuitionnistes, classiques et œcuméniques, avec ou sans polymorphisme prénexe ou sous-typage par prédicats, et le calcul des constructions. Les propriétés de correction, conservativité, cohérence, normalisation, et décidabilité de la vérification de type sont notamment établies pour les fragments des logiques œcuméniques du premier order et d'ordre supérieur sont établies.