Le programme produit par un système de programmation automatique, est obtenu en planifiant séparément les opérations de saisie, transport et montage des objets, et en ignorant les incertitudes géométriques (introduisant des interdépendances entre les actions). L'approche de vérification-correction de programme s'appuie sur un modèle incluant une représentation des incertitudes et s'appuie sur une description des actions des robots

Cette thèse de doctorat étudie l'interprétation calculatoire des preuves de la logique classique. Elle présente trois calculs reflétant trois approches différentes de la question. <br /><br /> Cette thèse est donc composée de trois parties. <br /><br /> La première partie introduit le *X calcul, dont les termes représentent des preuves dans le calcul des séquents classique. Les règles de réduction du *X calcul capture la plupart des caractéristiques de l'élimination des coupures du calcul des séquents. Ce calcul introduit des termes permettant une<br />implémentation implicite de l'effacement et de la duplication. Pour autant que nous sachions, c'est le premier tel calcul pour la logique classique. <br /><br /> La deuxième partie étudie la possibilité de représenter les calculs classiques au moyen de diagrammes. Nous présentons le dX calcul, qui est le calcul diagrammatique de la logique classique, et dont les diagrammes sont issus des<br />*X-termes. La différence principale réside dans le fait que dX fonctionne à un niveau supérieur d'abstraction. Il capture l'essence des preuves du calcul des séquents ainsi que l'essence de l'élimination classique des coupures. <br /><br /> La troisième partie relie les deux premières. Elle présente le $copy;X calcul qui est une version unidimensionnelle du calcul par diagramme. Nous commencons par le *X, où nous identifions explicitement les termes qui doivent l'être. Ceux-ci<br />sont les termes qui encodent les preuves des séquents qui sont équivalentes modulo permutation de règles d'inférence indépendantes. Ces termes ont également la même représentation par diagramme. Une telle identification induit une relation de congruence sur les termes. La relation de réduction est définie modulo la congruence, et les règles de réduction correspondent à celle du dX calcul.

Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées

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.

Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées / Finding a good paradigm to represent parallel programming in a simple and efficient way is a challenge currently faced by computer science research, mainly due to the evolution of machine architectures towards multi-core processors. BSML is a high level, structured parallel programming language that takes part in the research in an original way. By building upon existing work, this thesis extends the language and makes it more general, simple and usable with added imperative features such as references and exceptions, a specific syntax, etc. The existing formal and safety characteristics of the language (semantics, type system...) are preserved and extended. A major application is given in the form of a methodology for the development of fully proved parallel programs