This thesis describes a Coq formalization of realizability interpretations of arithmetic. The realizability interpretations are based on partial combinatory algebras—to each partial combinatory algebra there is an associated realizability interpretation. I construct two partial combinatory algebras. One of these gives a realizability interpretation equivalent to Kleene’s original one, without involving the usual recursion-theoretic machinery. / Den här uppsatsen beskriver en Coq-formalisering av realiserbarhetstolkningar av aritmetik. Realiserbarhetstolkningarna baseras på partiella kombinatoriska algebror—för varje partiell kombinatorisk algebra finns det en motsvarande realiserbarhetstolkning. Jag konstruerar två partiella kombinatoriska algebror. En av dessa ger en realiserbarhetstolkning som är ekvivalent med Kleenes ursprungliga tolkning, men dess konstruktion använder inte det sedvanliga rekursionsteoretiska maskineriet.

During the system and software development process for distributed systems, the development of the overall system design is critical for correctness, performance, and reliability. The objective of this thesis is the improvement of methods and tools that can be used to obtain a correct design model for distributed system components automatically by deriving the design model from the global system requirements. Mainly, we are concerned with the transformation from a global requirements model to a distributed design model. The global requirements model describes the behavior of a distributed system in an abstract manner by defining the local actions to be performed by different roles which represent actors in the different system components. The distributed design model defines the behavior of each actor separately, including its local actions plus the exchange of coordination messages, which are necessary to assure that the actions are performed in the required order. In this work, we first consider a global requirements model in the form of partially ordered actions similar to High-level Message Sequence Chart (HMSC). We study the realizability of the global requirements, which is said to be directly realizable if a design model can be constructed without any coordination messages. We study some problems which prevent direct realizability, such as strict sequence, non-local choice, non-deterministic choice, termination race, and others, and show under which conditions these problems are absent and the global model is directly realizable. For the other cases, we show how a conforming design model can be obtained by introducing a minimal number of coordination messages. In this context, we also show under which conditions sequence numbers are required in the messages of a weak while loop. Then we study the automatic derivation of a distributed design model using a tool. In order to obtain an easily readable notation for the global requirements model, we adapt the HMSC notation to the UML Hierarchical State Machine (HSM) notation and extend this notation to describe the roles that participate in the actions of each state of the global behavior. A simple state represents some local actions of a single role, while a hierarchical state usually represents a collaboration between several roles. Then we describe a derivation algorithm that can be applied to a global model written in this proposed HSM notation and generates a distributable UML HSM model, which contains a hierarchical state machine for each role of the application. We implemented this derivation algorithm as a tool in the context of the Umple UML development environment. This tool takes a global requirements model written in the extended HSM notation as input and automatically generates a UML HSM model. The distributed implementation environment described in Zakariapour’s thesis is used for generating a distributed Java implementation, where each distributed component contains one Java run-time environment and realizes the behavior of one or several of the roles of the application. A Travel Management System illustrative example has been discussed to illustrate the representation of the global model using the extended HSM notation and to demonstrate the correctness of the generated design models by the tool.

京都大学 / 0048 / 新制・課程博士 / 博士(理学) / 甲第20157号 / 理博第4242号 / 新制||理||1610(附属図書館) / 京都大学大学院理学研究科数学・数理解析専攻 / (主査)准教授 照井 一成, 教授 岡本 久, 教授 長谷川 真人 / 学位規則第4条第1項該当 / Doctor of Science / Kyoto University / DFAM

京都大学 / 新制・課程博士 / 博士(理学) / 甲第24393号 / 理博第4892号 / 新制||理||1699(附属図書館) / 京都大学大学院理学研究科数学・数理解析専攻 / (主査)教授 長谷川 真人, 教授 牧野 和久, 准教授 照井 一成 / 学位規則第4条第1項該当 / Doctor of Science / Kyoto University / DFAM

La réalisabilité classique de Jean-Louis Krivine associe à chaque modèle de calcul et chaque modèle de la théorie des ensembles un nouveau modèle de la théorie des ensembles, appelé modèle de réalisabilité, d'une façon similaire au forcing. Chaque modèle de réalisabilité est muni d’une algèbre de Boole caractéristique $\gimel 2$ (gimel 2), dont la structure donne des informations sur les propriétés du modèle de réalisabilité. En particulier, les modèles de forcing correspondent au cas où $\gimel 2$ est l'algèbre de Boole à deux éléments.Ce travail présente de nouveaux outils pour manipuler les modèles de réalisabilité et donne de nouveaux résultats obtenus en les exploitant. L'un d'entre eux est qu'au premier ordre, la théorie des algèbres de Boole à au moins deux éléments est complète pour $\gimel 2$, au sens où $\gimel 2$ eut être rendue élémentairement équivalente à n'importe quelle algèbre de Boole. Deux autres résultats montrent que $\gimel 2$ peut être utilisée pour étudier les modèles dénotationnels de langage de programmation (chacun part d'un modèle dénotationnel et classifie ses degrés de parallélisme à l'aide de $\gimel 2$). Un autre résultat montre que la technique de Jean-Louis Krivine pour réaliser l'axiome des choix dépendants à partir de l'instruction quote peut se généraliser à des formes plus fortes de choix. Enfin, un dernier résultat, obtenu en collaboration avec Laura Fontanella, accompagne le précédent en adaptant la condition d'antichaîne dénombrable du forcing au cadre de la réalisabilité, ce qui semble semble ouvrir une piste prometteuse pour réaliser l'axiome du choix. / Jean-Louis Krivine's classical realizability defines, from any given model of computation and any given model of set theory, a new model of set theory called the realizability model, in a similar way to forcing. Each realizability model is equipped with a characteristic Boolean algebra $\gimel 2$ (gimel 2), whose structure encodes important information about the properties of the realizability model. For instance, forcing models are precisely the realizability models in which $\gimel 2$ is the Boolean algebra with to elements.This document defines new tools for studying realizability models and exploits them to derive new results. One such result is that, as far as first-order logic is concerned, the theory of Boolean algebras with at least two elements is complete for $\gimel 2$, meaning that for each Boolean algebra B (with at least two elements), there exists a realizability model in which $\gimel 2$ is elementarily equivalent to B. Next, two results show that $\gimel 2$ can be used as a tool to study denotational models of programming languages (each one of them takes a particular denotational model and classifies its degrees of parallelism using $\gimel 2$). Moving to set theory, another results generalizes Jean-Louis Krivine's technique of realizing the axiom of dependant choices using the instruction quote to higher forms of choice. Finally, a last result, which is joint work with Laura Fontanella, complements the previous one by adapting the countable antichain condition from forcing to classical realizability, which seems to open a new, promising approach to the problem of realizing the full axiom of choice.

Service-oriented engineering is an emerging software development paradigm for distributed collaborative applications. Such an application is made up of several entities abstracted as services, each of them being for example a Web application, a Web service, or even a human. The services can be developed independently and are composed to achieve common requirements through interactions among them. Service choreographies define such requirements from a global perspective, based on interactions among a set of participants. This thesis aims to formalize the problems and attempts to develop a framework by which service choreographies can be developed correctly for both top-down and bottom-up approaches. It consists in analyzing the relation between a choreography specification and a choreography implementation at both model level and real implementation level. Particularly, it concerns the composition/decomposition service design, the verification, and the testing of choreography implementation. The first key point of our framework is to support value-passing among services by using symbolic technique and SMT solver. It overcomes false negatives or state space explosion issues due by abstracting or limiting the data domain of value-passing in existing approaches. The second key point is the black-box passive testing of choreography implementation. It does not require neither to access to source codes nor to make the implementation unavailable during the testing process. Our framework is fully implemented in our toolchains, which can be downloaded or used online at address: http://schora.lri.fr.

For a graph G, a set S is a dominating set if every vertex in V-S has a neighbor in S. A vertex contained in some minimum dominating set is called good; otherwise it is bad. A graph G has g(G) good vertices and b(G) bad vertices. The relationship between the order of G and g(G) assigns the graph to one of four classes. Our results include a method of classifying caterpillars. Further, we develop realizability conditions for a graph G given a triple of nonnegative integers representing the domination number of γ(G), g(G), and b(G), respectively, and provide constructions of graphs meeting those conditions. We define the goodness index of a vertex v in a graph G as the ratio of distinct γ(G)-sets containing v to the total number of γ(G)-sets, and provide formulas that yield the goodness index of any vertex in a given path.

Cette thèse étudie deux modèles de réalisabilité pour la logique classique construits sur la sémantique des jeux HO, interprétant la logique, l'arithmétique et l'analyse classiques directement par des programmes manipulant un espace de stockage d'ordre supérieur.La non-innocence en jeux HO autorise les références d'ordre supérieur, et le non parenthésage révèle la CPS des jeux HO et fournit une catégorie de continuations dans laquelle interpréter le lambda-mu calcul de Parigot. Deux modèles de réalisabilité sont construits sur cette interprétation calculatoire directe des preuves classiques.Le premier repose sur l'orthogonalité, comme celui de Krivine, mais il est simplement typé et au premier ordre. En l'absence de codage de l'absurdité au second ordre, une mu-variable libre dans les réaliseurs permet l'extraction. Nous définissons un bar-récurseur et prouvons qu'il réalise l'axiome du choix dépendant, utilisant deux conséquences de la structure de CPO du modèle de jeux: toute fonction sur les entiers (même non calculable) existe dans le modèle, et toute fonctionnelle sur des séquences est Scott-continue. La bar-récursion est habituellement utilisée pour réaliser intuitionnistiquement le « double negation shift » et en déduire la traduction négative de l'axiome du choix. Ici, nous réalisons directement l'axiome du choix dans un cadre classique.Le second, très spécifique au modèle de jeux, repose sur des conditions de gain: des ensembles de positions d'un jeu munis de propriétés de cohérence. Un réaliseur est alors une stratégie dont les positions sont toutes gagnantes. / This thesis investigates two realizability models for classical logic built on HO game semantics. The main motivation is to have a direct computational interpretation of classical logic, arithmetic and analysis with programs manipulating a higher-order store.Relaxing the innocence condition in HO games provides higher-order references, and dropping the well-bracketing of strategies reveals the CPS of HO games and gives a category of continuations in which we can interpret Parigot's lambda-mu calculus. This permits a direct computational interpretation of classical proofs from which we build two realizability models.The first model is orthogonality-based, as the one of Krivine. However, it is simply-typed and first-order. This means that we do not use a second-order coding of falsity, and extraction is handled by considering realizers with a free mu-variable. We provide a bar-recursor in this model and prove that it realizes the axiom of dependent choice, relying on two consequences of the CPO structure of the games model: every function on natural numbers (possibly non computable) exists in the model, and every functional on sequences is Scott-continuous. Usually, bar-recursion is used to intuitionistically realize the double negation shift and consequently the negative translation of the axiom of choice. Here, we directly realize the axiom of choice in a classical setting.The second model relies on winning conditions and is very specific to the games model. A winning condition is a set of positions in a game which satisfies some coherence properties, and a realizer of a formula is then a strategy which positions are all winning.

Cette thèse s'intéresse au contenu calculatoire des preuves classiques, et plus spécifiquement aux preuves avec effets de bord et à la réalisabilité classique de Krivine. Le manuscrit est divisé en trois parties, dont la première consiste en une introduction étendue des concepts utilisés par la suite. La seconde partie porte sur l’interprétation calculatoire de l’axiome du choix dépendant en logique classique. Ce travail s'inscrit dans la continuité du système dPAω d'Hugo Herbelin, qui permet d’adapter la preuve constructive de l’axiome du choix en théorie des types de Martin-Löf pour en faire une preuve constructive de l’axiome du choix dépendant dans un cadre compatible avec la logique classique. L'objectif principal de cette partie est de démontrer la propriété de normalisation pour dPAω, sur laquelle repose la cohérence du système. La difficulté d'une telle preuve est liée à la présence simultanée de types dépendants (pour la partie constructive du choix), d'opérateurs de contrôle (pour la logique classique), d'objets co-inductifs (pour "encoder" les fonctions de type N → A par des streams (a₀,a₁,...)) et d'évaluation paresseuse avec partage (pour ces objets co-inductifs). Ces difficultés sont étudiées séparément dans un premier temps. En particulier, on montre la normalisation du call-by-need classique (présenté comme une extension du λµµ̃-calcul avec des environnements partagé), en utilisant notamment des techniques de réalisabilité à la Krivine. On développe ensuite un calcul des séquents classique avec types dépendants, définie comme une adaptation du λµµ̃-calcul, dont la correction est prouvée à l'aide d'une traduction CPS tenant compte des dépendances. Enfin, une variante en calcul des séquents du système dPAω est introduite, combinant les deux points précédents, dont la normalisation est finalement prouvée à l'aide de techniques de réalisabilité. La dernière partie, d'avantage orientée vers la sémantique, porte sur l’étude de la dualité entre l’appel par nom (call-by-name) et l’appel par valeur (call-by-value) dans un cadre purement algébrique inspiré par les travaux autour de la réalisabilité classique (et notamment les algèbres de réalisabilité de Krivine). Ce travail se base sur une notion d'algèbres implicatives développée par Alexandre Miquel, une structure algébrique très simple généralisant à la fois les algèbres de Boole complètes et les algèbres de réalisabilité de Krivine, de manière à exprimer dans un même cadre la théorie du forcing (au sens de Cohen) et la théorie de la réalisabilité classique (au sens de Krivine). Le principal défaut de cette structure est qu’elle est très orientée vers le λ-calcul, et ne permet d’interpréter fidèlement que les langages en appel par nom. Pour remédier à cette situation, on introduit deux variantes des algèbres implicatives les algèbres disjonctives, centrées sur le “par” de la logique linéaire (mais dans un cadre non linéaire) et naturellement adaptées aux langages en appel par nom, et les algèbres conjonctives, centrées sur le “tenseur” de la logique linéaire et adaptées aux langages en appel par valeur. On prouve en particulier que les algèbres disjonctives ne sont que des cas particuliers d'algèbres implicatives et que l'on peut obtenir une algèbre conjonctive à partir d'une algèbre disjonctive (par renversement de l’ordre sous-jacent). De plus, on montre comment interpréter dans ces cadres les fragments du système L de Guillaume Munch-Maccagnoni en appel par valeur (dans les algèbres conjonctives) et en appel par nom (dans les algèbres disjonctives). / This thesis focuses on the computational content of classical proofs, and specifically on proofs with side-effects and Krivine classical realizability. The manuscript is divided in three parts, the first of which consists of a detailed introduction to the concepts used in the sequel.The second part deals with the computational content of the axiom of dependent choice in classical logic. This works is in the continuity of the system dPAω developed Hugo Herbelin. This calculus allows us to adapt the constructive proof of the axiom of choice in Martin-Löf's type theory in order to turn it into a constructive proof of the axiom of dependent choice in a setting compatible with classical logic. The principal goal of this part is to prove the property of normalization for dPAω, on which relies the consistency of the system. Such a proof is hard to obtain, due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of co-inductive objects (in order to "encode" functions of type N → A as streams (a₀,a₁,...)) and of lazy evaluation with sharing (for this co-inductive objects). These difficulties are first studied separately. In particular, we prove the normalization of classical call-by-need (presented as an extension of the λµ̃µ-calculus with shared environments) by means of realizability techniques. Next, we develop a classical sequent calculus with dependent types, defined again as an adaptation of the λµ̃µ-calculus, whose soundness is proved thanks to a CPS translation which takes the dependencies into account. Last, a sequent-calculus variant of dPAω is introduced, combining the two previous systems. Its normalization is finally proved using realizability techniques. The last part, more oriented towards semantics, studies the duality between the call-by-name and the call-by-value evaluation strategies in a purely algebraic setting, inspired from several works around classical realizability (and in particular Krivine realizability algebras). This work relies on the notion of implicative algebras developed by Alexandre Miquel, a very simple algebraic structure generalizing at the same time complete Boolean algebras and Krivine realizability algebras, in such a way that it allows us to express in a same setting the theory of forcing (in the sense of Cohen) and the theory of classical realizability (in the sense of Krivine). The main default of these structures is that they are deeply oriented towards the λ-calculus, and that they only allows to faithfully interpret languages in call-by-name. To remediate the situation, we introduce two variants of implicative algebras: disjunctive algebras, centered on the "par" connective of linear logic (but in a non-linear framework) and naturally adapted to languages in call-by-name; and conjunctives algebras, centered on the "tensor" connective of linear logic and adapted to languages in call-by-value. Amongst other things, we prove that disjunctive algebras are particular cases of implicative algebras and that conjunctive algebras can be obtained from disjunctive algebras (by reversing the underlying order). Moreover, we show how to interpret in these frameworks the fragments of Guillaume Munch-Maccagnoni's system L corresponding to a call-by-value calculus (within conjunctive algebras) and to a call-by-name calculus (within disjunctive algebras).

De nos jours, la simulation des écoulements diphasiques a de plus en plus d’importance dans les chambres de combustion aéronautiques en tant qu’un des éléments requis pour analyser et maîtriser le processus complet de combustion, afin d’améliorer la performance du moteur et de mieux prédire les émissions polluantes. Dans les applications industrielles, la modélisation du combustible liquide trouvé en aval de l’injecteur sous forme de brouillard de gouttes polydisperse, appelé spray, est de préférence faite à l’aide de méthodes Eulériennes. Ce choix s’explique par les avantages qu’offrent ces méthodes par rapport aux méthodes Lagrangiennes, notamment la convergence statistique intrinsèque, le couplage aisé avec la phase gazeuse ainsi que l’efficacité pour le calcul haute performance. Dans la présente thèse, on utilise une approche Eulérienne basée sur une fermeture au niveau cinétique de type distribution Gaussienne Anisotrope (AG). L’AG résout des moments de vitesse jusqu’au deuxième ordre et permet de capter les croisements des trajectoires (PTC) à petite échelle de manière statistique. Le système d’équations obtenu est hyperbolique, le problème est bien-posé et satisfait les conditions de réalisabilité. L’AG est comparé au modèle monocinétique (MK) d’ordre 1 en vitesse. Il est approprié pour la description des particules faiblement inertielles. Il mène à un système faiblement hyperbolique qui peut générer des singularités. Plusieurs schémas numériques, utilisés pour résoudre les systèmes hyperboliques et faible- ment hyperboliques, sont évalués. Ces schémas sont classifiés selon leur capacité à traiter les singularités naturellement présentes dans les modèles Eulériens, sans perdre l’ordre global de la méthode ni rompre les conditions de réalisabilité. L’AG est testé sur un champ turbulent 3D chargé de particules dans des simulations numériques directes. Le code ASPHODELE est utilisé pour la phase gazeuse et l’AG est implémenté dans le code MUSES3D pour le spray. Les résultats sont comparés aux de simulations Lagrangiennes de référence et aux modèle MK. L’AG est validé pour des gouttes modérément inertielles à travers des résultats qualitatifs et quantitatifs. Il s’avère prometteur pour les applications complexes comprenant des PTC à petite échelle. Finalement, l’AG est étendu à la simulation aux grandes échelles nécessaire dans les cas réels turbulents dans le domaine industriel en se basant sur un filtrage au niveau cinétique. Cette stratégie aide à garantir les conditions de réalisabilités. Des résultats préliminaires sont évalués en 2D pour tester la sensibilité des résultats LES sur les paramètres des modèles de fermetures de sous mailles. / In aeronautical combustion chambers, the ability to simulate two-phase flows gains increasing importance nowadays since it is one of the elements needed for the full understanding and prediction of the combustion process. This matter is motivated by the objective of improving the engine performance and better predicting the pollutant emissions. On the industrial scale, the description of the fuel spray found downstream of the injector is preferably done through Eulerian methods. This is due to the intrinsic statistical convergence of these methods, their natural coupling to the gas phase and their efficiency in terms of High Performance Computing compared to Lagrangian methods. In this thesis, the use of Kinetic-Based Moment Method with an Anisotropic Gaussian (AG) closure is investigated. By solving all velocity moments up to second order, this model reproduces statistically the main features of small scale Particles Trajectories Crossing (PTC). The resulting hyperbolic system of equations is mathematically well-posed and satisfies the realizability properties. This model is compared to the first order model in the KBMM hierarchy, the monokinetic model MK which is suitable of low inertia particles. The latter leads to a weakly hyperbolic system that can generate δ-shocks. Several schemes are compared for the resolution of the hyperbolic and weakly hyperbolic system of equations. These methods are assessed based on their ability to handle the naturally en- countered singularities due to the moment closures, especially without globally degenerating to lower order or violating the realizability constraints. The AG is evaluated for the Direct Numerical Simulation of 3D turbulent particle-laden flows by using ASPHODELE solver for the gas phase, and MUSES3D solver for the Eulerian spray in which the new model is implemented. The results are compared to the reference Lagrangian simulation as well as the MK results. Through the qualitative and quantitative results, the AG is found to be a predictive method for the description of moderately inertial particles and is a good candidate for complex simulations in realistic configurations where small scale PTC occurs. Finally, within the framework of industrial turbulence simulations a fully kinetic Large Eddy Simulation formalism is derived based on the AG model. This strategy of directly applying the filter on the kinetic level is helpful to devise realizability conditions. Preliminary results for the AG-LES model are evaluated in 2D, in order to investigate the sensitivity of the LES result on the subgrid closures.