Les travaux de cette thèse se situent dans le cadre de la linguistique computationnelle. La problématique est de définir une interface syntaxe / sémantique basée sur les théories de la grammaire générative.<br />Une première partie, concernant le problème de l'analyse syntaxique, présente tout d'abord, la syntaxe générative, puis un formalisme la réalisant: les grammaires minimalistes de Stabler. <br />À partir de ces grammaires, nous réalisons une étude sur les propriétés de l'opération de fusion pour laquelle nous définissons des notions d'équivalence, ainsi qu'une modélisation abstraite des lexiques.<br />Une seconde partie revient sur le problème de l'interface. Pour cela, nous proposons un formalisme de type logique, basé sur la logique mixte (possédant des connecteurs commutatifs et non-commutatifs), qui équivaut, sous certaines conditions, aux grammaires de Stabler. <br />Dans ce but, nous introduisons une normalisation des preuves de cette logique, normalisation permettant de vérifier la propriété de la sous-formule. Ces propriétés sont également étendues au calcul de Lambek avec produit.<br />À partir de l'isomorphisme de Curry-Howard, nous synchronisons un calcul sémantique avec les preuves réalisant l'analyse syntaxique. Les termes de notre calcul font appel aux propriétés du lambda mu-calcul, ainsi qu'à celles de la DRT (Discourse Representative Theory).<br />Une dernière partie applique ces formalismes à des cas concrets. Nous établissons des fragments d'une grammaire du français autour du problème des clitiques.

Le calcul de réécriture ou rho-calcul est une généralisation du lambda-calcul avec filtrage et agrégation de termes. L'abstraction sur les variables est étendue à une abstraction sur les motifs et le filtrage correspondant peut être effectué modulo une théorie <br />équationnelle a priori arbitraire. L'agrégation est utilisée pour collecter les différents résultats possibles.<br />Dans cette thèse, nous étudions différentes combinaisons des ingrédients fondamentaux du rho-calcul: le filtrage, l'agrégation et les mécanismes d'ordre supérieur.<br />Nous étudions le filtrage d'ordre supérieur dans le lambda-calcul pur modulo une restriction de la beta-conversion appelée super-développements. Cette nouvelle approche est suffisamment expressive pour traiter les problèmes de filtrage du second-ordre et ceux avec des motifs d'ordre supérieur à la Miller.<br />Nous examinons ensuite les modèles catégoriques du<br />lambda-calcul parallèle qui peut être vu comme un enrichissement du lambda-calcul avec l'agrégation de termes. Nous montrons que ceci est une étape significative vers la sémantique dénotationnelle du calcul de réécriture.<br />Nous proposons également une étude et une comparaison des calculs avec motifs éventuellement dynamiques, c'est-à-dire qui peuvent être instanciés et réduits. Nous montrons que cette étude, et plus particulièrement la preuve de confluence, est suffisamment générale pour<br />s'appliquer à l'ensemble des calculs connus. Nous étudions ensuite l'implémentation de tels calculs en proposant un calcul de réécriture avec filtrage et substitutions explicites.

Cette thèse couvre le sujet des systèmes de traitement de données àgrande échelle, et plus précisément trois approches complémentaires :la conception d'un système pour prédir des défaillances de serveursgrâce à l'analyse de leurs données de supervision; l'acheminement dedonnées dans un système à temps réel en étudiant les corrélationsentre les champs des messages pour favoriser la localité; etfinalement un environnement de développement innovateur pour concevoirdes transformations de donées en utilisant des graphes orientés deblocs.À travers le projet Smart Support Center, nous concevons unearchitecture qui passe à l'échelle, afin de stocker des sériestemporelles rapportées par des moteurs de supervision, qui vérifienten permanence la santé des systèmes informatiques. Nous utilisons cesdonnées pour effectuer des prédictions, et détecter de potentielsproblèmes avant qu'ils ne ne produisent.Nous nous plongeons ensuite dans les algorithmes d'acheminement pourles sytèmes de traitement de données en temps réel, et développons unecouche pour acheminer les messages plus efficacement, en évitant lesrebonds entre machines. Dans ce but, nous identifions en temps réelles corrélations qui apparaissent entre les champs de ces messages,tels les mots-clics et leur localisation géographique, par exempledans le cas de micromessages. Nous utilisons ces corrélations pourcréer des tables d'acheminement qui favorisent la colocation desacteurs traitant ces messages.Pour finir, nous présentons λ-blocks, un environnement dedéveloppement pour effectuer des tâches de transformations de donnéessans écrire de code source, mais en créant des graphes de blocs decode. L'environnement est rapide, et est distribué avec des pilesincluses: libraries de blocs, modules d'extension, et interfaces deprogrammation pour l'étendre. Il est également capable de manipulerdes graphes d'exécution, pour optimisation, analyse, vérification, outout autre but. / This thesis covers the topic of large-scale data processing systems,and more precisely three complementary approaches: the design of asystem to perform prediction about computer failures through theanalysis of monitoring data; the routing of data in a real-time systemlooking at correlations between message fields to favor locality; andfinally a novel framework to design data transformations usingdirected graphs of blocks.Through the lenses of the Smart Support Center project, we design ascalable architecture, to store time series reported by monitoringengines, which constantly check the health of computer systems. We usethis data to perform predictions, and detect potential problems beforethey arise.We then dive in routing algorithms for stream processing systems, anddevelop a layer to route messages more efficiently, by avoiding hopsbetween machines. For that purpose, we identify in real-time thecorrelations which appear in the fields of these messages, such ashashtags and their geolocation, for example in the case of tweets. Weuse these correlations to create routing tables which favor theco-location of actors handling these messages.Finally, we present λ-blocks, a novel programming framework to computedata processing jobs without writing code, but rather by creatinggraphs of blocks of code. The framework is fast, and comes withbatteries included: block libraries, plugins, and APIs to extendit. It is also able to manipulate computation graphs, foroptimization, analyzis, verification, or any other purposes.

S'assurer qu'un programme informatique se comporte bien, surtout dans des applications critiques (santé, transport, énergie, communications, etc.) est de plus en plus important car les ordinateurs et programmes informatiques sont de plus en plus omniprésents, voir essentiel au bon fonctionnement de la société. Mais comment vérifier qu'un programme se comporte comme prévu, quand les informations qu'il prend en entrée sont de très grande taille, voire de taille non bornée a priori ? Pour exprimer avec exactitude ce qu'est le comportement d'un programme, il est d'abord nécessaire d'utiliser un langage logique formel. Cependant, comme l'a montré Gödel dans, dans tout système formel suffisamment riche pour faire de l'arithmétique, il y a des formules valides qui ne peuvent pas être prouvées. Donc il n'y a pas de programme qui puisse décider si toute propriété est vraie ou fausse. Cependant, il est possible d'écrire un programme qui puisse vérifier la correction d'une preuve. Ce travail utilisera justement un tel programme, Coq, pour formellement vérifier la correction d'un certain programme. Dans cette thèse, nous expliquons le développement d'une nouvelle version de Rainbow, plus rapide et plus sûre, basée sur le mécanisme d'extraction de Coq. La version précédente de Rainbow vérifiait un certificat en deux étapes. Premièrement, elle utilisait un programme OCaml non certifié pour traduire un fichier CPF en un script Coq, en utilisant la bibliothèque Coq sur la théorie de la réécriture et la terminaison appelée CoLoR. Deuxièmement, elle appelait Coq pour vérifier la correction du script ainsi généré. Cette approche est intéressante car elle fournit un moyen de réutiliser dans Coq des preuves de terminaison générée par des outils extérieurs à Coq. C'est également l'approche suivie par CiME3. Mais cette approche a aussi plusieurs désavantages. Premièrement, comme dans Coq les fonctions sont interprétées, les calculs sont beaucoup plus lents qu'avec un langage où les programmes sont compilés vers du code binaire exécutable. Deuxièmement, la traduction de CPF dans Coq peut être erronée et conduire au rejet de certificats valides ou à l'acceptation de certificats invalides. Pour résoudre ce deuxième problème, il est nécessaire de définir et prouver formellement la correction de la fonction vérifiant si un certificat est valide ou non. Et pour résoudre le premier problème, il est nécessaire de compiler cette fonction vers du code binaire exécutable. Cette thèse montre comment résoudre ces deux problèmes en utilisant l'assistant à la preuve Coq et son mécanisme d'extraction vers le langage de programmation OCaml. En effet, les structures de données et fonctions définies dans Coq peuvent être traduits dans OCaml et compilées en code binaire exécutable par le compilateur OCaml. Une approche similaire est suivie par CeTA en utilisant l'assistant à la preuve Isabelle et le langage Haskell. / Making sure that a computer program behaves as expected, especially in critical applications (health, transport, energy, communications, etc.), is more and more important, all the more so since computer programs become more and more ubiquitous and essential to the functioning of modern societies. But how to check that a program behaves as expected, in particular when the range of its inputs is very large or potentially infinite? In this work, we explain the development of a new, faster and formally proved version of Rainbow based on the extraction mechanism of Coq. The previous version of Rainbow verified a CPF le in two steps. First, it used a non-certified OCaml program to translate a CPF file into a Coq script, using the Coq libraries on rewriting theory and termination CoLoR and Coccinelle. Second, it called Coq to check the correctness of the script. This approach is interesting for it provides a way to reuse in Coq termination proofs generated by external tools. This is also the approach followed by CiME3. However, it suffers from a number of deficiencies. First, because in Coq functions are interpreted, computation is much slower than with programs written in a standard programming language and compiled into binary code. Second, because the translation from CPF to Coq is not certified, it may contain errors and either lead to the rejection of valid certificates, or to the acceptance of wrong certificates. To solve the latter problem, one needs to define and formally prove the correctness of a function checking whether a certificate is valid or not. To solve the former problem, one needs to compile this function to binary code. The present work shows how to solve these two problems by using the proof assistant Coq and its extraction mechanism to the programming language OCaml. Indeed, data structures and functions de fined in Coq can be translated to OCaml and then compiled to binary code by using the OCaml compiler. A similar approach was first initiated in CeTA using the Isabelle proof assistant.

Avgasmängden som bensindrivna fordon tillåts släppa ut minskas hela tiden. Ett sätt att möta framtida krav, är att förbättra katalysatorns effektivitet. För att göra detta kan luft-bränsle-förhållandet regleras med avseende på syrelagringen i katalysatorn, istället för som idag, reglera mot stökiometriskt blandningsförhållande. Eftersom syrelagringen inte går att mäta med en givare behövs en modell som beskriver katalysatorns dynamiska egenskaper. Tre sådana modeller har undersökts, utvärderats och jämförts. Två av modellerna har implementerats i Matlab/Simulink och anpassats till mätningar från en experimentuppställning. För att kunna observera syrelagringen online valdes slutligen en av modellerna ut, och implementerades i ett Extended Kalman filter. Ytterligare arbete behöver läggas ner på den mest lovande modellen, och detsamma gäller för Kalmanfiltret, men på sikt förväntas resultaten kunna bli bra. / The legal amount of emissions that vehicles with spark ignited engines are allowed to produce are steadily reduced over time. To meet future emission requirements it is desirable to make the catalytic converter work in a more efficient way. One way to do this is to control the air-fuel-ratio according to the oxygen storage level in the converter, instead of, as is done today, always trying to keep it close to stoichiometric. The oxygen storage level cannot be measured by a sensor. Hence, a model describing the dynamic behaviors of the converter is needed to observe this level. Three such models have been examined, validated, and compared. Two of these models have been implemented in Matlab/Simulink and adapted to measurements from an experimental setup. Finally, one of the models was chosen to be incorporated in an extended Kalman filter (EKF), in order to make it possible to observe the oxygen storage level online. The model that shows best potential needs further work, and the EKF is working with flaws, but overall the results are promising.

La complexité implicite (ICC) vise à donner des caractérisations de classes de complexité dans des langages de programmation ou des logiques, sans faire référence à des bornes sur les ressources (temps, espace mémoire). Dans cette thèse, nous étudions l’approche de la logique linéaire à la complexité implicite. L’objectif est de donner des caractérisations de classes de complexité, à travers des variantes du lambda-calcul qui sont typables dans de tels systèmes. En particulier, nous considérons à la fois une perspective monovalente et une perspective polyvalente par rapport à l’ICC. Dans le premier cas, le but est de caractériser une hiérarchie de classes de complexité à travers un lambda-calcul élémentaire typé dans la logique linéaire élémentaire (ELL), où la complexité ne dépend que de l’interface d’un programme, c’est à dire son type. La deuxième approche rend compte à la fois des fonctions calculables en temps polynomial et de la normalisation forte, à travers des termes du lambda-calcul pur qui sont typés dans un système inspiré par la logique linéaire Soft (SLL); en particulier, par rapport à l’approche logique ordinaire, ici nous abandonnons la modalité “!” en faveur de l’emploi des types stratifiés, vus comme un raffinement des types intersection non associatifs, afin d’améliorer la typabilité et, en conséquence, l’expressivité. Enfin, nous explorons l’utilisation des types intersection, privés de certaines de leurs propriétés, vers une direction plus quantitative que l’approche qualitative habituelle, afin d’obtenir une borne sur le calcul de lambda-termes purs, en obtenant en plus une caractérisation de la normalisation forte. / In this thesis we explore the linear logic approach to implicit computational complexity, through the design of type assignment systems based on light linear logic, or heavily inspired by them, with the purpose of giving a characterization of one or more complexity classes, through variants of lambda-calculi which are typable in such systems. In particular, we consider both a monovalent and a polyvalent perspective with respect to ICC. In the first one the aim is to characterize a hierarchy of complexity classes through an elementary lambda-calculus typed in Elementary Linear Logic (ELL), where the complexity depends only on the interface of a term, namely its type. The second approach gives an account of both the functions computable in polynomial time and of strong normalization, through terms of pure lambda-calculus which are typed in a system inspired by Soft Linear Logic (SLL); in particular, with respect to the usual logical take, in the latter we give up the “!” modality in favor of employing stratified types as a refinement of non-associative intersection types, in order to improve typability and, as a consequence, expressivity.Finally we explore the use of intersection types, deprived of some of their usual properties, towards a more quantitative approach rather than the usual qualitative one, namely in order to compute a bound on the computation of pure lambda-terms, obtaining in addition a characterization of strong normalization.

Composições cerâmicas de CaxSr1-xTi1-yFeyO3-&delta;, x = 0, 0,5 e 1,0, y = 0 e 0,35, foram preparadas por meio de síntese reativa de CaCO3, SrCO3, TiO2 e Fe2O3 e pela técnica dos precursores poliméricos. Os pós-cerâmicos foram avaliados por meio de análise térmica (termogravimétrica e térmica diferencial), difração de raios X e microscopia eletrônica de varredura. Compactos cerâmicos sinterizados foram analisados por difração de raios X, microscopia eletrônica de varredura, microscopia de varredura por sonda e espectroscopia de impedância. A força eletromotriz gerada entre duas faces paralelas de amostras cilíndricas foi monitorada na faixa de temperatura 600 - 1100 oC para pressão parcial de oxigênio de ~50 ppm, utilizando-se uma bomba eletroquímica de oxigênio com transdutores de zircônia estabilizada com ítria. Foram refinadas, por meio de análise de Rietveld as estruturas cristalinas determinadas na análise por difração de raios X: perovskita cúbica (x = 0) e perovskita ortorrômbica (x 0). A condutividade elétrica foi analisada por medidas de espectroscopia de impedância na faixa de freqüências 5 Hz-13 MHz da temperatura ambiente até ~200 C. A deconvolução dos diagramas de impedância [-Z\"() x Z\'()] na faixa de temperaturas 300 < T(K) < 500 mostra dois semicírculos atribuídos às contribuições intragranular (grãos) e intergranular (contornos de grão) à resistividade elétrica. Os compactos sinterizado utilizando pós preparados pela síntese de estado sólido apresentam valores de resistividade intergranular e intragranular maiores que os compactos preparados com pós obtidos pela síntese química. O sinal elétrico (força eletromotriz) gerado sob exposição a oxigênio mostra que esses compostos podem ser utilizados em dispositivos sensores de oxigênio entre 600 e 1100C. Análises topográficas em microscópio de varredura por sonda em superfícies polidas e atacadas termicamente mostram detalhes morfológicos dos grãos, permitindo concluir que compactos sinterizados preparados com pós obtidos pela rota química são menos porosos que os preparados com pós obtidos pela rota convencional de síntese de estado sólido. Estes resultados estão de acordo com os resultados de medidas de espectroscopia de impedância. / CaxSr1-xTi1-yFeyO3-&delta;, x = 0, 0.5 and 1.0, y = 0 and 0.35, ceramic compounds were synthesized by reactive solid state synthesis of CaCO3, SrCO3, TiO2 and Fe2O3, and by the polymeric precursor technique. The ceramic powders were evaluated by thermogravimetry and differential thermal analysis, X-ray diffraction and scanning electron microscopy. Sintered ceramic pellets were analyzed by X-ray diffraction, scanning electron microscopy, scanning probe microscopy and impedance spectroscopy. The electromotive force resulting from the exposing the pellets to partial pressure de oxygen in the ~50 ppm in the 600-1100 oC range was monitored using an experimental setup consisting of an oxygen electrochemical pump with yttria-stabilized zirconia transducer and sensor. Rietveld analysis of the X-ray data allowed for determining the crystalline structures: cubic perovskite (y = 0) and orthorhombic perovskite (y 0). The electrical conductivity was determined by the two probe impedance spectroscopy measurements in the 5 Hz-13 MHz frequency range from room temperature to approximately 200 C. The deconvolution of the [-Z\"() x Z\'()] impedance diagrams in the 300 < T(K) < 500 range shows two semicircles due to intragranular (bulk) and intergranular (grain boundary) contributions to the electrical resistivity. Sintered pellets using powders prepared by the ceramic route present higher inter- and intragranular resistivity values than pellets prepared with chemically synthesized powders. The emf signal under exposure oxygen shows that these compounds may be used in oxygen sensing devices in the 600 - 1100 C range. Scanning probe microscopy topographic analysis of the polished and thermally etched surfaces of the pellets gave details of grain morphology, showing that pellets prepared with powders synthesized by the chemical route are less porous than the ones obtained by the ceramic route. These results are in agreement with the impedance spectroscopy results.

Le lambda-calcul est un formalisation de la notion de calcul. Dans cette thèse nous nous intéresserons à certaines variantes non déterministes, et nous nous pencherons plus particulièrement sur le cas probabiliste.L'étude du lambda-calcul probabiliste n'est pas nouvelle, mais les travaux précédents considéraient le comportement probabiliste comme un effet de bord. Notre objectif est de présenter ce calcul d'une manière plus équationnelle, en intégrant le comportement probabiliste à la réduction.Tout d'abord nous définissons une sémantique opérationnelle déterministe et contextuelle pour le lambda-calcul probabiliste en appel par nom. Afin de traduire la signification de la somme nous définissons une équivalence syntaxique dans notre calcul, dont nous démontrons qu'il ne déforme pas la réduction: considérer une réduction modulo équivalence revient à considérer simplement le résultat du calcul modulo équivalence. Nous prouvons également un résultat de standardisation.Dans ce cadre nous définissons une notion de théorie équationnelle pour le lambda-calcul probabiliste. Nous étendons certaines notions usuelles, et en particulier celle de bon sens. Cette dernière se formalise facilement dans un cadre déterministe mais est bien plus complexe dans le cas probabiliste.Pour finir nous prouvons une correspondance entre l'équivalence observationnelle, l'égalité des arbres de Böhm et la théorie cohérente sensée maximale. Nous définissons une notion d'arbres de Böhm probabilistes dont nous prouvons qu'elle forme un modèle. Nous démontrons ensuite un résultat de séparabilité disant que deux termes avec des arbres de Böhm distincts ne sont pas observationnellement équivalents. / The lambda-calculus is a way to formalize the notion of computation. In this thesis we will be interested in some of these variants introducing non deterministim, and we will focus mostly on a probabilistic calculus.The probabilistic lambda-calculus has been studied for some time, but the probabilistic behaviour has always been treated as a side effect. Our purpose is to give a more equational representation of this calculus, by handling the probabilities inside the reduction rather than as a side effect.To begin with we give a deterministic and contextual operational semantics for the call-by-name probabilistic lambda-calculus. To express the probabilistic behaviour of the sum we introduce a syntactic equivalence in our calculus, and we show it has little consequence on the calculus: reducing modulo equivalence amount to reducing and then looking at the result modulo equivalence. We also prove a standardization theorem.Then using this operational semantics we define a notion of equational theories for the probabilistic lambda-calculus. We extend some usual notions to this setting, and in particular the sensibility of a theory. This notion is quite simple in a deterministic setting but becomes more complicated when we have a probabilistic computation.Finally we prove a generalization of the equality between the observational equivalence, the Böhm tree equality and the maximal coherent sensible lambda-theory. We give a notion of probabilistic Böhm trees, and prove that this forms a model of the probabilistic lambda-calculus. Then we prove a separability result stating that two terms with different Böhm trees are separable, i.e. are not observationally equivalent.

The globalized economy has incentivized Swedish companies to invest abroad, especially in emerging markets. When expanding into foreign markets companies must evaluate the adhering risks associated with that particular market. It is paramount that companies account for the country risk in their investment analysis, as any miscalculations could have detrimental effects on a company. Evaluating country risk has proven to be difficult due to the sheer range of aspects that may affect an investment. This study examines the required return on equity of Swedish companies in six different markets, and compares it to three different evaluation models in order to determine what variables constituted any misevaluations. Our analysis indicated that a majority of Swedish companies require too high return on equity compared to the empirical results of the applied model. / Globaliseringens utveckling har lett till att svenska investeringar på utländska marknader och ”emerging markets” ökat under de senaste åren. När företag expanderar till utländska marknader tillkommer nya risker som måste beaktas. Således har landsrisken blivit en väsentlig del av värderingen. Landsrisken har visat sig varit svårvärderad då det finns ett antal aspekter som måste beaktas. En eventuell felbedömning kan ha förödande konsekvenser för ett företag. Denna studie undersöker svenska företags avkastningskrav på sex olika marknader gentemot tre värderingsmodeller, och vilka faktorer som påverkat en potentiell fel värdering. Studien visar att majoriteten av de svenska företagen har ett högre avkastningskrav än vad de tillämpade modellerna beräknat.

Les cellules dendritiques {DC) jouent un rôle majeur dans l'induction de l'immunité anti-tumorale spécifique de l'antigène {Ag). Récemment, les DC BDCA3high humaines sont apparues comme étant homologues aux DC CD8a+ connues pour activer très efficacement les lymphocytes T CD8 par présentation croisée d'Ag chez la souris. Par ailleurs, ces deux populations de DC sont les productrices principales d'interféron-λ{IFN-λ), une cytokine récemment découverte et possédant des propriétés antivirales, antiprolifératives et anti-tumorales. Mon travail de thèse a permis de mieux caractériser la présentation croisée d'Ag cellulaire par les DC BDCA3high à l'aide d'un modèle in vitro et de mettre en lumière le rôle des cellules NK dans l'induction de ce processus. Ce travail a également aboutit à la mise en évidence des DC BDCA3high dans les tumeurs de sein et de révéler l'inhibition de leur sécrétion d'IFN-λ par des facteurs solubles présents dans le microenvironnement tumoral. L'ensemble de ces résultats devraient permettre de concevoir de nouvelles stratégies thérapeutiques basées sur le ciblage des DC BDCA3high / Dendritic cells {DC) play a major role in the induction of antigen {Ag) specific anti-tumoral immunity. Recently, human BDCA3high DC appeared to be homologous with CD8a+ DC known to activate very efficiently T CD8 lymphocyte by Ag cross-presentation in mice. Moreover, those two DC populations are the main producers of interferon-λ {IFN-λ), a recently discovered cytokine family with antiviral, anti-proliferative and anti-tumoral properties. My works participated to better characterize cell derived Ag cross-presentation by BDCA3high DC using an in vitro model and enlightened the role of NK cells in its induction. This works also end up in revealing the presence of BDCA3high DC in breast tumors and the inhibition of their IFN-λsecretion by soluble factor from tumor microenvironment. Altogether, those results should allow designing new anti-tumoral immunotherapeutic strategies based on BDCA3high DC targeting