Le présent manuscrit constitue la partie écrite du travail de thèse réalisé par Bruno Mery sous la direction de Christian Bassac et Christian Retoré entre 2006 et 2011, portant sur le sujet "Modélisation de la sémantique lexicale dans la théorie des types". Il s'agit d'une thèse d'informatique s'inscrivant dans le domaine du traitement automatique des langues, et visant à apporter un cadre formel pour la prise en compte, lors de l'analyse sémantique de la phrase, d'informations apportées par chacun des mots. Après avoir situé le sujet, cette thèse examine les nombreux travaux l'ayant précédée et s'inscrit dans la tradition du lexique génératif. Elle présente des exemples de phénomènes à traiter, et donne une proposition de système de calcul fondée sur la logique du second ordre. Elle examine ensuite la validité de cette proposition par rapport aux exemples et aux autres approches déjà formalisées, et relate une implémentation de ce système. Enfin, elle propose une brève discussion des sujets restant en suspens.

La plupart des programmes informatiques sont concurrents : ils doivent effectuer plusieurs tâches en même temps. Les threads et les événements sont deux techniques usuelles d'implémentation de la concurrence. Les événements sont généralement plus légers et efficaces que les threads, mais aussi plus difficiles à utiliser. De plus, ils sont souvent trop limités ; il est alors nécessaire d'écrire du code hybride, encore plus complexe, utilisant à la fois des threads ordonnancés préemptivement et des événements ordonnancés coopérativement. Nous montrons dans cette thèse que des programmes concurrents écrits dans un style à threads sont traduisibles automatiquement en programmes à événements équivalents et efficaces par une suite de transformations source-source prouvées. Nous proposons d'abord Continuation-Passing C, une extension du langage C pour l'écriture de systèmes concurrents qui offre des threads très légers et unifiés (coopératifs et préemptifs). Les programmes CPC sont transformés par le traducteur CPC pour produire du code à événements séquentialisé efficace, utilisant des threads natifs pour les parties préemptives. Nous définissons et prouvons ensuite la correction de ces transformations, en particulier le lambda lifting et la conversion CPS, pour un langage impératif. Enfin, nous validons la conception et l'implémentation de CPC en le comparant à d'autres bibliothèques de threads et en exhibant notre seeder BitTorrent Hekate. Nous justifions aussi notre choix du lambda lifting en implémentant eCPC, une variante de CPC utilisant les environnements, et en comparant ses performances à celles de CPC.

The fully quantum mechanical 'direct-potential-fit' (DPF) method has become increasingly widely used in the reduction of diatomic spectra. The central problem of this method is the representation of the potential energy and Born-Oppenheimer breakdown (BOB) correction functions. There are a number of problems associated with the existing method and potential forms. This thesis delineates these problems and finds solutions to some of them. In particular, it is shown that use of a different expansion variable and a new treatment of some of the expansions resolves most of the problems. These techniques have been successfully tested on the ground electronic states of the coinage metal hydrides and the Rb2 molecule. To address the problem of representing 'barrier' potential curves, a flexible new functional form, the 'double-exponential long-range' (DELR) potential function, is introduced and applied to the B barrier state of Li2. In addition, the Lambda-doubling level splitting which occurs for singlet Pi electronic states has been taken into account by extending the effective Schrodinger equation. The computer program DSPotFit developed in our laboratory for performing DPF analyses has been extended to incorporate the ability to fit the analytical potential energy functions to tunneling predissociation line widths for quasibound levels. Finally, an attempt is made to investigate whether there exists a hump in the ground state rotationless potential curve of beryllium hydride.

The fully quantum mechanical 'direct-potential-fit' (DPF) method has become increasingly widely used in the reduction of diatomic spectra. The central problem of this method is the representation of the potential energy and Born-Oppenheimer breakdown (BOB) correction functions. There are a number of problems associated with the existing method and potential forms. This thesis delineates these problems and finds solutions to some of them. In particular, it is shown that use of a different expansion variable and a new treatment of some of the expansions resolves most of the problems. These techniques have been successfully tested on the ground electronic states of the coinage metal hydrides and the Rb2 molecule. To address the problem of representing 'barrier' potential curves, a flexible new functional form, the 'double-exponential long-range' (DELR) potential function, is introduced and applied to the B barrier state of Li2. In addition, the Lambda-doubling level splitting which occurs for singlet Pi electronic states has been taken into account by extending the effective Schrodinger equation. The computer program DSPotFit developed in our laboratory for performing DPF analyses has been extended to incorporate the ability to fit the analytical potential energy functions to tunneling predissociation line widths for quasibound levels. Finally, an attempt is made to investigate whether there exists a hump in the ground state rotationless potential curve of beryllium hydride.

Any analysis of higher-order languages must grapple with the tri-facetted nature of lambda. In one construct, the fundamental control, environment and data structures of a language meet and intertwine. With the control facet tamed nearly two decades ago, this work brings the environment facet to heel, defining the environment problem and developing its solution: environment analysis. Environment analysis allows a compiler to reason about the equivalence of environments, i.e., name-to-value mappings, that arise during a program's execution. In this dissertation, two different techniques-abstract counting and abstract frame strings-make this possible. A third technique, abstract garbage collection, makes both of these techniques more precise and, counter to intuition, often faster as well. An array of optimizations and even deeper analyses which depend upon environment analysis provide motivation for this work. In an abstract interpretation, a single abstract entity represents a set of concrete entities. When the entities under scrutiny are bindings-single name-to-value mappings, the atoms of environment-then determining when the equality of two abstract bindings infers the equality of their concrete counterparts is the crux of environment analysis. Abstract counting does this by tracking the size of represented sets, looking for singletons, in order to apply the following principle: If {x} = {y}, then x = y. Abstract frame strings enable environmental reasoning by statically tracking the possible stack change between the births of two environments; when this change is effectively empty, the environments are equivalent. Abstract garbage collection improves precision by intermittently removing unreachable environment structure during abstract interpretation.

L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des Constructions a été présenté en 1985 par Thierry Coquand. Il s'agit d'un lambda-calcul typé qui, à travers l'isomorphisme dit de Curry-Howard, peut-être vu comme un formalisme logique. Ce système qui étend à la fois la logique d'ordre superieur de Church et les systèmes de Martin-Löf est particulièrement expressif du point de vue algorithmique et peut facilement être mis en oeuvre sur ordinateur.<br />Dans le Calcul des Constructions originel, les types de données (entiers, listes, sommes, etc) sont représentés dans le lambda-calcul à travers un codage imprédicatif. Cette solution est élégante mais conduit à un certain nombre de difficultés pratiques et théoriques. Pour y remédier, Thierry Coquand et Christine Paulin-Mohring on proposé d'étendre le formalisme par un mécanisme génerique de définitions inductives. C'est cette extension, utilisée dans le système Coq, qui est étudiée dans cette thèse. Le résultat essentiel est que le système vérifie bien la proprieté de normalisation forte. On en déduit les proprietés de cohérence logique, de confluence et de décidabilité du typage.<br />L'aspect le plus spectaculaire de l'extension par des types inductifs est la possibilité de définir de nouveaux types et de nouvelles propositions par récurrence structurelle (élimination forte). Cette caractéristique, qui donne toute sa signification à la notion de types dépendants, augmente énormément le pouvoir de la règle de conversion, et par là, la difficulté de la preuve de normalisation. L'interprétation de l'élimination forte dans une preuve de normalisation par réductibilité est la nouveauté essentielle de ce travail.<br />De plus, nous considérons ici un système avec eta-conversion. Une conséquence est que la propriété de confluence n'est plus combinatoire et doit être prouvée après la normalisation, ce qui augmente à nouveau la difficulté de la preuve de celle-ci. A ce titre, nous présentons également quelques résultats nouveaux sur des systèmes non-normalisants qui montrent que pour des lambda-calculs typés, la propriété de confluence est logique et non combinatoire.

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.

The increasing size of the car fleet makes it important to find ways of lowering the amounts of pollutants from each individual diesel or gasoline engine to almost zero levels. The pollutants from these engines predominantly originate from emissions at cold start, in the case when gasoline is utilized, and high NOx emissions and particulates from diesel engines. The cold start emissions from gasoline vehicles are primarily due to a high light-off time for the catalytic converter. Another reason is the inability to quickly heat the sensor used for controlling the air-to-fuel ratio in the exhausts, also called the lambda value, which is required to be in a particular range for the catalytic converter to work properly. This problem may be solved utilizing another, more robust sensor for this purpose. One way of treating the high NOx levels from diesel engines is to introduce ammonia in the exhausts and let it react with the NOx in a special catalytic converter to form nitrogen gas and water, which is called SCR (selective catalytic reduction). However, in order to make this system reduce NOx efficiently enough for meeting future legislations, closed loop control is required. To realize this type of system an NOx or ammonia sensor is needed. This thesis presents the efforts made to test the SiC-based field effect sensor device both as a cold start lambda sensor for gasoline engines and as an NH3 sensor for SCR systems in diesel engines. The MISiC (metal insulator silicon carbide) lambda sensor has proven to be both sensitive and selective to lambda, and its properties have been studied in lambda stairs both in gasoline engine exhausts and in the laboratory. There is, however, a small cross-sensitivity to CO. The influence of metal gate restructuring on the linearity of the sensor has also been investigated. The metal tends to form islands by time, which decreases the catalytic activity and thereby gives the sensor, which is binary when fresh, a linear behavior. Successful attempts to prevent the restructuring through depositing a protective layer of insulator on top of the metal were made. The influence of increasing the catalytic activity in the measurement cell was also studied. It was concluded that the location of the binary switch point of MISiC lambda sensors could be moved towards the stoichiometric value if the consumption of gases in the measurement cell was increased. The MISiC NH3 sensor for SCR systems has been shown to be highly sensitive to ammonia both in laboratory and diesel engine measurements. The influence of other diesel exhaust gas components, such as NOx, water or N2O has been found to be low. In order to make the ammonia sensor more long-term stable experiments on samples with different types of co-sputtered Pt or Ir/SiO2 gas-sensitive layers were performed. These samples turned out to be sensitive to NH3 even though they were dense and NH3 detection normally requires porous films. The speed of response for both sensor types has been found to be fast enough for closed loop control in each application. / On the day of the ublic defence of the doctoral thesis, the status of article IV was: accepted, article V was: submitted and article VII was: manuscript.

L'expérience ALICE auprès du LHC se propose d'étudier le passage de la matière du gaz de hadrons vers l'état de Plasma de Quarks et de Gluons où les partons sont déconfinés. Les collisions d'ions lourds ultra-relativistes présentent en effet la possibilité de créer des conditions de température et de pression extrêmes, nécessaires au déconfinement de la matière. Dans le cadre de cette étude, les collisions élémentaires proton-proton sont d'une importance certaine puisqu'elles constituent une référence hadronique. L'objectif de cette thèse a été de préparer l'étude des mécanismes de production des baryons et mésons étranges dans les collisions proton-proton aux énergies du LHC par la mesure des lambda et K0s avec ALICE. Les particules étranges constituent un outil majeur pour sonder la matière créée. Le comportement du rapport lambda/K0s aux impulsions transverses intermédiaires dans les collisions proton-proton à haute énergie, étudié au travers de différents modèles théoriques, pourrait également signer la présence de phénomènes collectifs, phénomènes jusqu'alors uniquement observés dans les collisions d'ions lourds.