Suivant la proposition de Tarski (1936), la sémantique vériconditionnelle associeà une phrase déclarative des conditions de vérité. Ainsi, comprendre le sens dela phrase “Il pleut”, c’est pouvoir dire après avoir regardé par la fenêtre si elle estvraie ou fausse. Toutefois, ceci ne permet de rendre compte que des phrases déclaratives,et pas des questions puisqu’aucune situation ne rendra jamais la question“Qui a appelé ce matin ?” vraie ou fausse. Hamblin (1973) propose la premièrethéorie des questions dans le cadre de la sémantique véri-conditionnelle, et proposede leur associer des conditions de résolutions, c’est-à-dire des ensembles deréponses. Comprendre le sens de la question “Qui a appelé ce matin ?” c’est alorssavoir que “Jean a appelé” est une réponse possible, tandis que “il pleuvait” n’enest pas une.Très rapidement, l’étude de la sémantique des questions s’est tournée versles questions enchâssées dans des phrases déclaratives (questions indirectes). Eneffet, il est beaucoup plus aisé de juger des conditions de vérité d’une phrasesdéclarative que des conditions de résolution d’une question. Or moyennant deshypothèses sur la sémantique des verbes enchâssant des questions (‘savoir’, ‘oublier’.. . ), on peut relier les conditions de vérité d’une phrase déclarative au sensde la question qu’elle enchâsse. Cette approche, proposée par Karttunen (1977), adonné lieu à une littérature théorique très riche. / Two important questions arise from the recent literature on embedded questions.First, Heim (1994) proposed that embedded questions are ambiguous betweena weakly and strongly exhaustive reading. Spector (2005) recently proposedan intermediate exhaustive reading as well. Second, adverbs of quantity such as’mostly’ can quantify over answers to an embedded questions (Berman, 1991). Ananalysis of this phenomena reveals an analogy between embedded questions andplural determiner phrases, and suggests a fine-grained structures for the denotationof questions (Lahiri, 2002).The first part of the dissertation consist of three psycholinguistic studies on theexhaustive readings of questions under ‘know’ in English, the acquisition of thesereadings under ‘savoir’ by French 5-to-6-ear-olds, and the properties of emotivefactivepredicates such as ‘surprise’. The second part presents a theory of embeddedquestions built on Klinedinst and Rothschild’s (2011) proposal to derive exhaustivereadings as implicatures, although it differs in the fine-grained structureit adopts for questions denotations in order to account for plurality effects as well.The theory solves problem raised by B. R. George (2013) and makes predictions fora larger range of sentences.

Cette thèse traite de la restriction en français et fournit tout d'abord une « grammaire » de la restriction à partir de la description fine des unités restrictives telles "seul" (Seule Marie a vu Emma), "seulement" (Marie a seulement vu Emma), et "ne... que" (Marie n'a vu Emma qu'hier), ainsi qu'un modèle sémantique du phénomène. Elle rend ensuite compte de trois études sémantiques motivées par la complexité de certaines données. La première s'intéresse à l'interaction entre syntagmes nominaux et restriction. On observe que la grammaticalité d'une phrase composée d'un SN modifié par la restriction dépend de contraintes non pas syntaxiques mais sémantiques et pragmatiques. La seconde étude traite de l'application du principe de l'association avec le focus valable pour "only" (Jackendoff, 1972) à l'équivalent français "seulement". La validité du principe est remise en question à partir d'une étude sémantique inspirée par Vallduvi et Zacharski (1994), et d'une expérimentation prosodique, étude pilote sur les données du français. Enfin, la troisième étude propose de représenter compositionnellement la contribution sémantique de la restriction. En prolongeant le travail initié par Rooth (1985,1992), nous mettons en évidence que la contribution de la restriction ne peut pas toujours être représentée de la même façon et est fonction de la profondeur de l'élément modifié syntaxiquement par la restriction et/ou de l'élément auquel s'associe la restriction.

Intuitivement, une simulation graphique (monde virtuel, jeu,...) peut etre vue comme un espace borne dans lequel plusieurs entites, disposant chacune d'un comportement propre, evoluent en parallele. Il parait donc naturel d'utiliser des langages concurrents pour programmer ces comportements. Cependant, c'est rarement le cas pour des raisons de complexite de programmation et de deboguage, de non-determinisme et d'efficacite. Nous proposons d'utiliser l'Approche Reactive introduite par F. Boussinot qui permet de definir clairement les comportements d'entites graphiques. Nous avons enrichi les Icobjs qui est un modele d'objets reactifs graphiques. Il offre la possibilite a des non-specialistes de construire graphiquement des comportements complexes a partir de comportements simples et de constructeurs graphiques. Nous avons realise une implementation dont l'objet central est Icobj. Il definit une structure minimale dynamiquement extensible pour permettre une construction graphique generique. Un icobj particulier, le Workspace, execute et affiche les icobjs qu'il contient. Les comportements sont executes par un moteur reactif dedie aux Icobjs appele Reflex. Il reprend les principales primitives du formalisme Junior en modifiant la semantique de certaines instructions et en y ajoutant de nouvelles. Toutes les instructions sont formalisees par des regles de reecritures au format SOS. De plus, nous avons developpe un environnement qui permet d'interagir dynamiquement avec les simulations. Enfin, nous presentons quelques experimentations autour de l'utilisation des Icobjs dans le cadre de simulations distribuees, de simulations physiques ou de simulations multi-horloges.

Cette thèse présente une perspective relationnelle à plusieurs aspects de la programmation. L'algèbre relationnelle de Tarski est utilisée pour formuler, et parfois résoudre, des problèmes pertinents à la programmation tels que: la spécification de programmes, l'analyse fonctionnellle de programmes, la vérification de programmes, la conception de programmes et le traitement d'erreurs dans les programmes. La perspective que nous adoptons dans cette thèse est caractérisée par les prémisses suivantes: les programmes sont spécifiés à l'aide de relations; l'analyse fonctionnellle de programmes se fait par composition de fonctions; la conception de programmes se fait par décomposition de relations

La programmation par aspects est un paradigme de programmation qui permet de mieux séparer les préoccupations d'une application. Un aspect est défini pour chaque préoccupation qui ne peut pas être isolée dans un module. Les aspects sont ensuite ajoutés au programme de base par un processus automatique appelé tissage. Cependant, l'expressivité des langages d'aspect généraux permet de modifier totalement la sémantique du programme de base (par ex., un aspect peut remplacer certains appels de méthode par du code arbitraire). Ce comportement peut entraîner la perte des avantages (lisibilité, maintenabilité, réutilisabilité, etc.) d'une meilleure modularisation des préoccupations. Il devient impossible de raisonner sur le programme de base sans regarder le programme tissé. Cette thèse apporte une réponse aux problèmes ci-dessus en définissant des catégories d'aspects dont l'impact sur la sémantique du programme de base reste sous contrôle. Pour chaque catégorie d'aspects, nous déterminons l'ensemble des propriétés du programme de base qui est préservé par tissage. L'appartenance d'un aspect à une catégorie est garantie par construction grâce à des langages d'aspect dédiés pour chaque catégorie. L'utilisation de ces langages assure que le tissage préservera l'ensemble des propriétés associé à la catégorie concernée. Les propriétés préservées sont représentées comme des sous ensembles de LTL et de CTL*. Nous prouvons formellement que quelque soit le programme de base, le tissage de n'importe quel aspect d'une catégorie préserve les propriétés de la catégorie correspondante. Ces langages et catégories sont définis dans un cadre formel indépendant de tout langage de base ou d'aspect. L'expressivité de ce cadre est montrée en décrivant des primitives complexes de langages d'aspect comme AspectJ et CaesarJ et en effectuant une preuve de correction de transformation d'aspect.

Cette thèse propose une nouvelle approche du parallélisme et de la concurrence, posant les bases d'un langage de programmation à la fois sûr et "secure" (garantissant la sécurité des données), fondé sur une sémantique formelle claire et simple, tout en étant adapté aux architectures multi-cœur. Nous avons adopté le paradigme synchrone, dans sa variante réactive, qui fournit une alternative simple à la programmation concurrente standard en limitant l'impact des erreurs dépendant du temps ("data-races"). Dans un premier temps, nous avons considéré un langage réactif d'orchestration, DSL, dans lequel on fait abstraction de la mémoire (Partie 1). Dans le but de pouvoir traiter la mémoire et la sécurité, nous avons ensuite étudié (Partie 2) un noyau réactif, CRL, qui utilise un opérateur de parallélisme déterministe. Nous avons prouvé la réactivité bornée des programmes de CRL. Nous avons ensuite équipé CRL de mécanismes pour contrôler le flux d'information (Partie 3). Pour cela, nous avons d'abord étendu CRL avec des niveaux de sécurité pour les données, puis nous avons défini dans le langage étendu, SSL, un système de types permettant d'éviter les fuites d'information. Parallèlement (Partie 4), nous avons ajouté la mémoire à CRL, en proposant le modèle DSLM. En utilisant une notion d'agent, nous avons structuré la mémoire de telle sorte qu'il ne puisse y avoir de "data-races". Nous avons également étudié l'implémentation de DSLM sur les architectures multi-cœur, fondée sur la notion de site et de migration d'un agent entre les sites. L'unification de SSL et de DSLM est une piste pour un travail futur.

Cette thèse étudie quelques préverbes et prépositions en bulgare (v/v-, iz/iz-) et en français (dans, hors de, en-/in-, ex-/é-) dans le cadre de la sémantique cognitive et formelle et plus particulièrement dans celui de la Grammaire Applicative et Cognitive (GAC). La formalisation à l’aide d’un schème quasi-topologique utilisant des lieux abstraits permet de construire des représentations adéquates et de dégager un invariant abstrait pour chaque unité étudiée. L’analyse aboutit à la construction d’une carte sémantique des significations d’intériorité et d’extériorité étudiées qui met en évidence les similarités, les différences et les oppositions entre les significations des différents préverbes et prépositions au sein d’une même langue ainsi qu’entre les deux langues, bulgare et français. Les résultats obtenus montrent que chaque langue construit ses propres représentations à partir de primitives invariantes et que, bien que les emplois des unités étudiées soient souvent très proches, il n’est pas possible d’établir des équivalences absolues entre significations. Cette étude contribue à argumenter en faveur de l’hypothèse anti-anti-relativiste de la GAC. / This thesis analyses some preverbs and prepositions in Bulgarian (v/v-, iz/iz-) and in French (dans, hors de, en-/in-, é-/ex-) within the framework of the cognitive and formal semantics, the Cognitive and Applicative Grammar (CAG) in particular. The formalisation using quasi-topological scheme and abstract loci allows the construction of appropriate representations and the formulation of an abstract invariant meaning for each item. The analysis leads to the construction of a semantic map of the interior and exterior meanings of the studied items which underlines the similarities, the differences and the oppositions between the meanings of different preverbs and prepositions within a single language as well as between the two languages, Bulgarian and French. The results of the analysis show that each language builds its own representations using invariant primitives and that, even if some of the studied meanings are very similar, it is impossible to establish absolute equivalencies between them. This study contributes to argue for the anti-anti-relativist hypothesis of the CAG.

La vérification formelle de programme n'apporte pas de garantie complète si l'outil de vérification est incorrect. Et, si un programme est vérifié au niveau source, le compilateur pourrait introduire des bugs. Les compilateurs et vérifieurs actuels sont complexes. Pour simplifier l'analyse et la transformation de code, ils utilisent des représentations intermédiaires (IR) de programme, qui ont de fortes propriétés structurelles et sémantiques. Cette thèse étudie d'un point de vue sémantique et formel les IRs, afin de faciliter la preuve de ces outils. Nous étudions d'abord une IR basée registre du bytecode Java. Nous prouvons un théorème sur sa génération, explicitant ce que la transformation préserve (l'initialisation d'objet, les exceptions) et ce qu'elle modifie et comment (l'ordre d'allocation). Nous implantons l'IR dans Sawja, un outil de développement d'analyses statiques de Java. Nous étudions aussi la forme SSA, une IR au coeur des compilateurs et vérifieurs modernes. Nous implantons et prouvons en Coq un middle-end SSA pour le compilateur C CompCert. Pour la preuve des optimisations, nous prouvons un invariant sémantique de SSA clé pour le raisonnement équationnel. Enfin, nous étudions la sémantique des IRs de Java concurrent. La définition actuelle du Java Memory Model (JMM) autorise les optimisations aggressives des compilateurs et des architectures parallèles. Complexe, elle est formellement cassée. Ciblant les architectures x86, nous proposons un sous-ensemble du JMM intuitif et adapté à la preuve formelle. Nous le caractérisons par ses réordonnancements, et factorisons cette preuve sur les IRs d'un compilateur. / An end-to-end guarantee of software correctness by formal verification must consider two sources of bugs. First, the verification tool must be correct. Second, programs are often verified at the source level, before being compiled. Hence, compilers should also be trustworthy. Verifiers and compilers' complexity is increasing. To simplify code analysis and manipulation, these tools rely on intermediate representations (IR) of programs, that provide structural and semantic properties. This thesis gives a formal, semantic account on IRs, so that they can also be leveraged in the formal proof of such tools. We first study a register-based IR of Java bytecode used in compilers and verifiers. We specify the IR generation by a semantic theorem stating what the transformation preserves, e.g. object initialization or exceptions, but also what it modifies and how, e.g. object allocation. We implement this IR in Sawja, a Java static analysis toolbench. Then, we study the Static Single Assignment (SSA) form, an IR widely used in modern compilers and verifiers. We implement and prove in Coq an SSA middle-end for the CompCert C compiler. For the proof of SSA optimizations, we identify a key semantic property of SSA, allowing for equational reasoning. Finally, we study the semantics of concurrent Java IRs. Due to instruction reorderings performed by the compiler and the hardware, the current definition of the Java Memory Model (JMM) is complex, and unfortunately formally flawed. Targetting x86 architectures, we identify a subset of the JMM that is intuitive and tractable in formal proofs. We characterize the reorderings it allows, and factor out a proof common to the IRs of a compiler.

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérificationdes systèmes temporisés. La première partie concerne une méthode de spécification enutilisant les diagrammes états-transitions pour modéliser un système donné en partant d’unedescription textuelle. Cette méthode guide l’utilisateur pour le développement de la modélisation.Elle comporte plusieurs étapes et utilise des observateurs d’états et des événements afind’engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de laméthode de spécification pour une application semi-automatique est présenté. La seconde partieconcerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, cequi permet d’utiliser les méthodes de vérification. Nous prenons en considération dans cette traductionun ensemble important des éléments syntaxiques des diagrammes états-transitions, telsque la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passageautomatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.La dernière partie concerne l’intégration des contraintes temporelles dans les deuxapproches précédentes. Nous définissons des annotations pour les diagrammes états-transitionsdont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dansla méthode de spécification et la traduction. Le but est de proposer des annotations faciles àcomprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plusutilisées. / In order to specify and verify timed systems, we present in this thesis approaches using UMLstate machines and coloured Petri nets. Our first approach is a specification method that takesinto account a textual description of the system and generates the corresponding state machinediagram. This method helps a non-expert user to model a system in a structural way. We presenta tool that implements the specification method. Our second approach is the translation of UMLstate machine diagrams to coloured Petri nets diagrams. In this approach we take into account animportant set of UML state machine elements that allows the modelling of concurrent systems,etc. A tool that implements the approach and allows us to automate the translation is beingdeveloped. Finally, the last approach is the integration of time constraints in our specificationmethod and in our translation. We propose a set of annotations to model time in state machinediagrams, and we define the corresponding syntax and semantics.

Dans cette thèse, on présente un cadre qui associe la spécification algèbrique de types à l'algèbre de programme. La principale caractéristique de cette approche est fournie par les opérateurs génériques définissables par les utilisateurs qui donnent une grande puissance d'expression aux règles d'équivalence. En particulier, la structure de certains types est contenue implicitement dans des opérateurs génériques comme l'homomorphisme et l'homomorphisme «inverse». Les applications de cette algèbre de programmes typés incluent la preuve de programmes sans induction explicite, et les méthodes de transformation de programmes comme le «folding-unfolding»