Le travail présenté dans cette thèse concerne l'étude de la notion de conversion inhérente à tous système de types dépendants. Plusieurs présentations de ces systèmes ont été étudiées pour des usages variés: typage, recherche de preuve, cohérence de logique... Chacune de ces représentation est accompagnée d'une notion d'égalité différente, suivant les besoins du moment. Mais il n'est pas certains que toutes ces représentations parlent en fin de compte d'une seule et même logique. Nous nous intéressons ici à une famille assez conséquente de systèmes de types, appelés Systèmes de Types Purs, et nous allons prouver que pour ces systèmes, toutes les représentations habituellement utilisées sont en fait équivalentes, c'est à dire qu'il existe des traductions constructives entre chacune de ces présentations. Ces traductions reposent toutes sur la manière de porter une égalité d'un système à l'autre. Ce travail se concentre donc sur les mécanismes de ces égalités, et prouve qu'il est possible de typer n'importe quelle égalité syntaxique en égalité sémantique, et ainsi qu'il est donc possible de passer d'un système à l'autre. L'intégralité de cette thèse a en outre été vérifiée et certifiée correcte à l'aide de l'assistant à la preuve Coq, qui a activement été utilisé tout au long de l'élaboration des preuves. ~

Dans ce document, nous montrons comment la notion de calculabilité introduite par W. W. Tait et étendue par Girard aux types polymorphes peut être utilisée et facilement étendue pour montrer la terminaison de différents types de relations de réécriture, y compris avec filtrage sur des symboles définis, filtrage d'ordre supérieur ou réécriture de classe modulo certaines théories équationnelles. Nous montrons également que la notion de clôture de calculabilité donne lieu a une relation bien fondée incluant l'extension à l'ordre supérieur par J.-P. Jouannaud et A. Rubio de l'ordre récursif sur les chemins de N. Dershowitz.

Proteins are dynamic and interconvert between different conformations to perform their biological functions. Simulation methodology drawing upon principles from classical mechanics - molecular dynamics (MD) simulation - can be used to simulate protein dynamics and reconstruct the conformational ensemble at a level of atomic detail that is inaccessible to experiment. We use the dynamic insight achieved through simulation to enhance our understanding of protein structures solved by X-ray crystallography. Protein X-ray structures provide the most important information for structural biology, yet they depict just a single snapshot of the solution ensemble, which is under the influence of the confined crystal medium. Thus, we ask a fundamental question - how well do static X-ray structures represent the dynamic solution state of a protein? To understand how the crystal environment affects both global and local protein conformational dynamics, we consider two model systems. We first examine the variation in global conformation observed in several solved X-ray structures of the λ Cro dimer by reconstructing the solution ensemble using the replica exchange enhanced sampling method, and show that one X-ray conformation is unstable in solution. Subsequent simulation of Cro in the crystal environment quantitatively assesses the strength of packing interfaces and reveals that mutation in the lattice affects the stability of crystal forms. We also evaluate the Cro models solved by nuclear magnetic resonance spectroscopy and demonstrate that they represent unstable solution states. In addition to our studies of the Cro dimer, we investigate the effect of crystal packing on side-chain conformational dynamics through solution and crystal MD simulation of the HIV microbicide Cyanovirin-N. We find that long, polar surface side-chains can undergo a strong reduction in conformational entropy upon incorporation into crystal contacts, which supports the application of surface engineering to facilitate protein crystallization. Finally, we outline a general framework for using network visualization to aid in the functional interpretation of conformational ensembles generated from MD simulation. Our results will enhance the understanding of X-ray data in establishing protein structure-function-dynamics relationships.

While the car fleet becomes increasingly larger it is important to lower the amounts of pollutants from each individual diesel or gasoline engine to almost zero levels. The pollutants from these engines predominantly originate from high NOx emissions and particulates, in the case when diesel is utilized, and emissions at cold start from gasoline engines. One way of treating the high NOx levels is to introduce ammonia in the diesel exhausts and let it react with the NOx 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. 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. This thesis presents the efforts made to test the SiC-based field effect transistor (SiC-FET) sensor technology both as an ammonia sensor for SCR systems and as a cold start lambda sensor. The SiC-FET sensor has been shown to be highly sensitive to ammonia both in laboratory and engine measurements. As a lambda sensor it has proven to be both sensitive and selective, and its properties have been studied in lambda stairs both in engine exhausts and in the laboratory. The influence of metal gate restructuring on the linearity of the sensor has also been investigated. The speed of response for both sensor types has been found to be fast enough for closed loop control in each application. / <p>On the day of the public defence of the doctoral thesis, the status of article III was: in press. Report code: LiU-Tek-Lic-2003:50.</p>

Immunoglobulins are proteins produced by plasma cells and humans normally produce five different immunoglobulin classes of IgG, IgA, IgM, IgD and IgE. The basic function of the immunoglobulins is to counteract the invasion of pathogenic organisms by their antibody activity and to protect against its toxic products. The basic structure of the immunoglobulins is made up of two identical heavy chains and two light chains, kappa and lambda. In healthy subjects, normal plasma cell contents of the bone marrow are 1-3 %, in patients with multiple myeloma (MM), concentrations increase to over 90 % and are comprised of a malignant transplanted plasma cell clone. This clone of cells produces a kind of immunoglobulin that can be detected using various laboratory methods in both serum and urine. Analysis of free light immunoglobulin chains (kappa and lambda) in human serum occurs in the diagnosis and follow-up of MM and provides a simpler and faster alternative to daily urine collection for the analysis of light immunoglobulin chains in the urine. The purpose of the study was to carry out a method verification of free light chains in serum using an automated immunochemical instrument, BN Prospec II from Siemens, which uses the nephelometric measuring principle (antigen-antibody complex). The calibration concentrations of kappa and lambda assigned by Siemens were met. The method's stability and precision were measured by analyzing high and low controls for both analytes in each of the internal and total series. Within the series received CV 1,47 % for SL1 kappa and 2,57 % for SL2 kappa, and 1,77 % for SL1 lambda and 2,57 % for SL2 lambda. The total series was obtained CV 1,58 % for SL1 kappa and 2,81 % for SL2 kappa and CV 2,05 % for SL1 lambda and 2,30 % for SL2 lambda. The correctness of the method was studied through a patient comparison where 64 patient samples previously analyzed in Lund were analyzed in Kalmar. The study showed good precision and repeatability, the results of the patient comparison showed good correspondence with corresponding methods performed in Lund when the coefficient of determination for S-FLC-kappa was 0, 999 and 0, 958 for S-FLC-lambda. The conclusion is that analysis of free light chains in serum can be used in routine operation in the laboratory for clinical chemistry and transfusion medicine at the county hospital in Kalmar.

Made available in DSpace on 2017-03-14T14:10:08Z (GMT). No. of bitstreams: 0 Previous issue date: 2015-10-01. Added 1 bitstream(s) on 2017-03-14T14:42:49Z : No. of bitstreams: 1 000874637.pdf: 3049251 bytes, checksum: 612105d6db96ee6a9d1d53c4cf9e159e (MD5) / Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP) / Essencial para o desempenho de posicionamento baseado em redes é que um usuá- rio receba e aplique as informações de correção geradas a partir de uma rede. Essas correções são necessárias para o usuário levar em conta os atrasos atmosféricos (ionosfera e troposfera) entre a sua localização aproximada e as estações da rede. A m de proporcionar correções mais precisas para os usuários, o processamento da rede deve ser baseada na solução das ambiguidades inteiras da fase da portadora entre as estações da rede. Denomina-se ambiguidade o número de ciclos inteiros entre as antenas do satélite e do receptor na primeira época de coleta de dados. As ambiguidades são introduzidas como parâmetros a serem estimados nas equações de observação. processo de solução das ambiguidades pode ser dividido em duas etapas: estimação e de validação. A estimativa está preocupada com o cálculo dos valores das ambiguidades. o etapa de validação é utilizada para inferir se o valor estimado pode ser aceito ou não. Um método muito utilizado pela comunidade cientí ca internacional para a estimação das ambiguidades inteiras é o método LAMBDA. Já para a validação os testes Ratio e FF-RT podem ser utilizados. O objetivo desta dissertação é investigar a solução das ambiguidades no contexto do posicionamento baseado em redes e sua implementação no software FCT_RTK_Net que foi desenvolvido em ambiente acadêmico. Nesta dissertação alguns experimentos sobre a solução das ambiguidades são apresentados, cujos resultados mostraram que o teste de validação FF-RT produz melhores percentuais de xação das ambiguidades. Os resultados também mostraram que o ADOP é um bom preditor da taxa de sucesso das ambiguidades e que a detecção e correção de perdas de ciclos são essenciais para a obtenção da solução das ambiguidades / Essencial to the performance of Network RTK positioning is that a user receives and applies correction information from a network. These corrections are necessary for the user to account for the atmospheric (ionospheric and tropospheric) delays between his approximate location and the locations of the network's stations. In order to provide the most precise corrections to users, the network processing should be based on integer resolution of the carrier phase ambiguities between the network's stations. Ambiguity is called the number of complete cycles between the satellite antenna and receiver in his rst season of data collection. The ambiguities are introduced as parameters to be estimated in the observation equations. Ambiguity resolution can be divided in two steps: estimation and validation. The estimate is concerned with the calculation of the ambiguities values. O validation stage is used to infer whether the estimated value can be accepted or not. A method widely used by the international scienti c community for the estimation of integer ambiguities is the LAMBDA method. For the validation the ratio test and FF-RT may be used. The aim of this work is to investigate the resolution of ambiguities in the context of Network RTK and its implementation in FCT_RTK_Net software that was developed in an academic environment. In this thesis some experiments on resolving the ambiguities are presented, the results showed that the FF-RT validation test produces better percentage xing the ambiguities. The results also showed that ADOP is a good predictor of the success rate of ambiguities and that the detection and correction cycles slips are essential for obtaining the resolution of ambiguities / FAPESP: 2013/06325-9

Avec les espaces de finitude, Ehrhard a exhibé une sémantique de la logique linéaire contenant une opération de différentiation. Dans ce cadre, l'interprétation des formules est décomposable en séries de Taylor. Cette étude a engendré des syntaxes différentielles. Cette thèse de sémantique dénotationnelle prolonge ce travail par une exploration de sémantiques vectorielles de la logique linéaire, et contribue à l'étude sémantique et syntaxique de la formule de Taylor. La première partie aborde la sémantique. Nous présentons l'interprétation des constructions de la logique linéaire dans les espaces vectoriels munis d'une topologie linéarisée, les espaces de Lefschetz. Nous définissons une notion intrinsèque d'espaces de finitude, les espaces de Lefschetz finitaires. Nous caractérisons les espaces de Lefschetz réflexifs complets à l'aide de bornologies linéaires. Enfin, nous montrons que la décomposition de Taylor reste valide dans ces espaces. La seconde partie porte sur les syntaxes différentielles. La formule de Taylor syntaxique traduit un terme en une superposition de termes différentiels qui sont autant de possibilités d'exécutions. Comme l'ont montré Ehrhard et Regnier, les termes issus de cette traduction vérifient une relation de cohérence. Nous introduisons une sémantique totale qui capture cette relation. Puis, nous construisons une extension vectorielle du lambda-calcul, le calcul barycentrique, interprété par cette sémantique totale. Enfin, dans le cadre des réseaux différentiels, nous présentons un algorithme non déterministe qui permet de décider si un ensemble fini de réseaux différentiels provient de la traduction d'un réseau de la logique linéaire par la formule de Taylor syntaxique.

La notion de théorie s'est séparée de la notion de logique à la fin des années 1920, lorsque Hilbert et Ackermann ont distingué les règles de déduction, indépendantes de l'ob jet du discours, des axiomes qui lui sont spécifiques. S'est alors posée la question de caractériser les théories, définies donc comme des ensembles d'axiomes, que l'on peut utiliser pour formaliser une partie du raisonnement mathématique. Un premier critère est la cohérence de cette théorie : le fait qu'on ne puisse pas démontrer toutes les propositions de cette théorie. Cependant il est progressivement apparu que la cohérence n'était pas une propriété suffisante. Le fait que les démonstrations constructives vérifient les propriétés de la dijonction ou du témoin, ou la complétude de certaines méthodes de démonstration automatique ne découlent pas de la seule cohérence d'une théorie. Mais toutes trois sont par contre conséquentes d'une même propriété : la normalisation des démonstrations. En 1930, le théorème de complétude de Gödel montra que le critére de cohérence pouvait être vu sous différents angles. En plus de la définition précédente interne à la théorie de la démonstration, on peut également définir de manière algébrique la cohérence d'une théorie comme le fait qu'elle possède un modèle. L'équivalence entre ces deux définitions constitue un outil fondamental, qui a permis notamment la démonstration de la cohérence de nombreuses théories : la théorie des ensembles avec la négation de l'axiome du choix par Fraenkel et Mostovski, la théorie des ensembles avec l'axiome du choix et l'hypothèse du continue par Gödel, la théorie des ensembles avec la négation de l'hypothèse du continu par Cohen, . . . A l'inverse, la normalisation des démonstrations semblait ne pouvoir se définir que de manière interne à la théorie de la démonstration. Certains critères inspirés de la théorie des modèles étaient certes parfois utilisés pour démontrer la propriété de normalisation des démonstrations de certaines théories, mais la nécéssité de ces critéres n'avait pas été établie. Nous proposons dans cette thèse un critère algébrique à la fois nécessaire et suffisant pour la normalisation des démonstrations. Nous montrons ainsi que la propriété de normalisation des démonstrations peut également se définir comme un critère algébrique, à l'instar de la propriété de cohérence. Nous avons pour cela défini une nouvelle notion d'algèbre de valeurs de vérités (TVA) appelée algèbres de vérité dépendant du langage (LDTVA). La notion de TVA permet d'exhiber l'algèbre de valeurs de vérité des candidats de réductibilité définis par Girard en 1970. L'existence d'un modèle à valeurs dans cette algèbre définit un critère algébrique suffisant pour la propriété de normalisation des démonstrations. Puis nous avons défini un raffinement de la notion de candidats de réductibilité comme une de ces LDTVAs et avons montré que l'existence d'un modèle à valeurs dans cette algèbre définit un critère algébrique toujours suffisant mais également nécessaire pour la propriété de normalisation des démonstrations. Ce critère est défini pour les cadres logiques de la déduction minimale et du λΠ-calcul modulo. Et nous exhibons finalement la puissance du λΠ-calcul modulo en montrant que tous les systèmes de types purs fonctionnels peuvent être simulés dans ce cadre logique.

La Géométrie de l'Interaction (GdI) de Girard est une sémantique des langage de programmations tenant compte de leur dynamique de réduction.<br />Dans un premier temps, on présente les réseaux d'interaction de Lafont comme une instance particulière de GdI. Puis, on définis un cadre général d'étude de la GdI à partir d'un ensemble de symboles et de règles d'interaction.<br />Dans un second temps, on introduit une notion de concision associée à la GdI et on montre dans quelle mesure cette notion fait du sens à l'aide d'une famille d'exemple basée sur les entiers de Church.<br />Dans un dernier temps, on présente les réseaux d'interaction différentiels d'Ehrhard et Regnier et on définit leur GdI. On montre que la théorie usuelle de Danos-Regnier est entièrement récupérée.

L'objet de cette thèse est l'étude des systèmes formels du type des systèmes LJ et LK de Gentzen (couramment appelés calculs des séquents) dans leur rapport avec la calculabilité. Le procédé de calcul dans ces systèmes consiste en « l'élimination des coupures ». Deux interprétations sont considérées.<br /><br />Le lambda-calcul constitue le support de la première interprétation. Nous établissons une correspondance de type Curry-Howard entre LJ et une variante syntaxique du lambda-calcul avec opérateur explicite de substitution (de type « let _ in _ »). Une procédure de normalisation/élimination des coupures confluente et terminant fortement est donnée et l'extension de la correspondance à LK se fait en considérant l'opérateur mu du lambda-mu-calcul de Parigot.<br /><br />La théorie des jeux constitue le support de la deuxième interprétation: les preuves des calculs des séquents sont vues comme des stratégies gagnantes pour certains types de jeux à deux joueurs (dialogues) se disputant la validité de la formule prouvée. Nous donnons deux résultats.<br /><br />Dans un premier temps, nous montrons qu'il suffit de considérer des restrictions LJQ de LJ puis LKQ de LK pour établir, dans le cas propositionnel, une bijection entre les preuves de ces systèmes et les E-dialogues intuitionnistes puis classiques définis par Lorenzen dans un but de fondement de la prouvabilité en termes de jeux. Ceci affine et généralise un résultat de Felscher d'équivalence entre l'existence d'une preuve d'une formule A dans LJ et l'existence d'une stratégie gagnante pour le premier des joueurs dans un E-dialogue à propos de A.<br /><br />Dans un deuxième temps, nous partons d'une logique propositionnelle infinitaire sans variable considérée par Coquand pour y définir une interaction prouvée terminante entre les preuves vues comme stratégies gagnantes. Nous montrons une correspondance opérationnelle entre ce procédé d'interaction et l'élimination « faible de tête » des coupures, celle-ci étant indépendamment prouvée terminante.