De plus en plus de calculs de surveillance, contrôle etc. sont effectués de façon logicielle. Notre objectif est de prouver formellement des calculs numériques qui offrent déjà un premier niveau de garantie sur leurs résultats, comme des calculs par intervalles, et en particulier des calculs avec des modèles de Taylor.<br /><br />Cette thèse présente la construction d'une bibliothèque de modèles de Taylor pour l'assistant de preuves PVS. Nous avons développé les modèles de Taylor pour les opérations d'addition, soustraction, multiplication par un scalaire, multiplication, élévation au carré, puissance et racine carrée. Nous avons également développé les modèles de Taylor pour l'exponentielle, le sinus, l'arctangente et les sinus et cosinus hyperboliques. Nous avons démontré dans PVS que les opérations et fonctions définies dans notre bibliothèque préservent la propriété d'inclusion, travail de preuve qui n'avait pas été fait auparavant dans les implantations des modèles de Taylor.<br /><br />Nous avons développé une stratégie PVS pour certifier des inégalités ou bornes d'expressions. Quand on utilise un assistant de preuves pour démontrer une inégalité, il peut être nécessaire de guider l'assistant pas à pas dans la démonstration. Pour cette raison, les utilisateurs effectuent rarement la démonstration. Par conséquent, simplifier la façon de prouver les inégalités et bornes d'expressions facilite l'utilisation de PVS.<br /><br />Notre bibliothèque peut être utilisée pour construire des modèles de Taylor pour des expressions données, pour dériver des bornes plus ou moins précises pour des expressions arithmétiques et également pour certifier des inégalités ou bornes d'expressions. Disposer d'une méthode pour vérifier des expressions dans un assistant de preuves permet de vérifier certaines expressions qui apparaissent dans des logiciels de missions critiques.<br /><br />Pour résumer, nous avons développé une bibliothèque de modèles de Taylor en PVS qui comprend les opérations arithmétiques et certaines fonctions élémentaires. Nous avons démontré la propriété d'inclusion pour les opérations et fonctions développées. Nous avons développé une stratégie appelée containment pour démontrer la propriété d'inclusion des modèles de Taylor construits à partir des opérations et fonctions précédemment définies. Nous avons développé une stratégie appelée taylors pour prouver des inégalités en utilisant les modèles de Taylor. Nous avons illustré sur deux applications l'intérêt de ces développements.

Dans cette thèse, nous visons à formaliser les effets calculatoires. En effet, les langages de programmation les plus utilisés impliquent différentes sortes d'effets de bord: changement d'état, exceptions, entrées / sorties, non-déterminisme, etc. Ils peuvent apporter facilité et flexibilité dans le processus de codage. Cependant, le problème est de prendre en compte les effets lorsque l'on veut prouver des propriétés de programmes. La principale difficulté dans ce genre de preuve de programmes est le décalage entre la syntaxe des opérations avec effets de bord et leur interprétation. Typiquement, un fragment de programme avec des arguments de type X qui retourne une valeur de type Y n'est pas interprété comme une fonction de X vers Y , à cause des effets.L'approche algébrique la plus connue pour ce problème permet une interprétation des programmes, y compris ceux comportant des effets, en utilisant des monades : l'interprétation est une fonction de X vers T (Y ) où T est une monade. Cette approche a été étendue aux théories de Lawvere et aux "gestionnaires algébriques" (algebraic handlers). Une autre approche, appelée logique décorée, fournit une sémantique équationnelle pour ces programmes. Nous spécialisons l'approche de la logique décorée pour les effets liés à l'état de la mémoire et à la gestion des exceptions en définissant la logique décorée pour les états (L_st) et la logique décorée pour les exceptions (L_exc), respectivement. Elles nous permettent de prouver des propriétés de programmes impliquant de tels effets. Ensuite, nous formalisons ces logiques en Coq et certifions les preuves associées. Ces logiques sont construites de manière à être correctes. En outre, nous introduisons une notion de complétude syntaxique relative d'une théorie dans une logique donnée par rapport à une sous-logique. Nous montrons que la théorie décorée pour les états globaux ainsi que deux théories décorées pour les exceptions sont relativement complets relativement à leur sous-logique pure. Non seulement nous pouvons utiliser le système développé pour prouver des programmes comportant des effets, mais également nous utilisons cette formalisation pour certifier les résultats de complétude obtenus. / In this thesis, we aim to formalize the effects of a computation. Indeed, most used programming languages involve different sorts of effects: state change, exceptions, input/output, non-determinism, etc. They may bring ease and flexibility to the coding process. However, the problem is to take into account the effects when proving the properties of programs. The major difficulty in such kind of reasoning is the mismatch between the syntax of operations with effects and their interpretation. Typically, a piece of program with arguments in X that returns a value in Y is not interpreted as a function from X to Y , due to the effects. The best-known algebraic approach to the problem interprets programs including effects with the use of monads: the interpretation is a function from X to T(Y) where T is a monad. This approach has been extendedto Lawvere theories and algebraic handlers. Another approach called, the decorated logic, provides a sort of equational semantics for reasoning about programs with effects. We specialize the approach of decorated logic to the state and the exceptions effects by defining the decorated logic for states (L_st) and the decorated logic for exceptions (L_exc), respectively. This enables us to prove properties of programs involving such effects. Then, we formalize these logics in Coq and certify the related proofs. These logics are built so as to be sound. In addition, we introduce a relative notion of syntactic completeness of a theory in a given logic with respect to a sublogic. We prove that the decorated theory for the global states as well as two decorated theories for exceptions are syntactically complete relatively to their pure sublogics. These proofs are certified in Coq as applications of ourgeneric frameworks.