L'objet de cette thèse est l'extension des méthodes de la théorie des types intersections non-idempotents, introduite par Gardner et de Carvalho, à des cadres dépassant le lambda-calcul stricto sensu.- Nous proposons d'abord une caractérisation de la normalisation de tête et de la normalisation forte du lambda-mu calcul (déduction naturelle classique) en introduisant des types unions non-idempotents. Comme dans le cas intuitionniste, la non-idempotence nous permet d'extraire du typage des informations quantitatives ainsi que des preuves de terminaison beaucoup plus élémentaires que dans le cas idempotent. Ces résultats nous conduisent à définir une variante à petits pas du lambda-mu-calcul, dans lequel la normalisation forte est aussi caractérisée avec des méthodes quantitatives. - Dans un deuxième temps, nous étendons la caractérisation de la normalisation faible dans le lambda-calcul pur à un lambda-calcul infinitaire étroitement lié aux arbres de Böhm et dû à Klop et al. Ceci donne une réponse positive à une question connue comme le problème de Klop. À cette fin, il est nécessaire d'introduire conjointement un système (système S) de types infinis utilisant une intersection que nous qualifions de séquentielle, et un critère de validité servant à se débarrasser des preuves dégénérées auxquelles les grammaires coinductives de types donnent naissance. Ceci nous permet aussi de donner une solution au problème n°20 de TLCA (caractérisation par les types des permutations héréditaires). Il est à noter que ces deux problèmes n'ont pas de solution dans le cas fini (Tatsuta, 2007).- Enfin, nous étudions le pouvoir expressif des grammaires coinductives de types, en dehors de tout critère de validité. Nous devons encore recourir au système S et nous montrons que tout terme est typable de façon non triviale avec des types infinis et que l'on peut extraire de ces typages des informations sémantiques comme l'ordre (arité) de n'importe quel lambda-terme. Ceci nous amène à introduire une méthode permettant de typer des termes totalement non-productifs, dits termes muets, inspirée de la logique du premier ordre. Ce résultat prouve que, dans l'extension coinductive du modèle relationnel, tout terme a une interprétation non vide. En utilisant une méthode similaire, nous montrons aussi que le système S collapse surjectivement sur l'ensemble des points de ce modèle. / In this dissertation, we extend the methods of non-idempotent intersection type theory, pioneered by Gardner and de Carvalho, to some calculi beyond the lambda-calculus.- We first present a characterization of head and strong normalization in the lambda-mu calculus (classical natural deduction) by introducing non-idempotent union types. As in the intuitionistic case, non-idempotency allows us to extract quantitative information from the typing derivations and we obtain proofs of termination that are far more elementary than those in the idempotent case. These results leads us to define a small-step variant of the lambda-mu calculus, in which strong normalization is also characterized by means of quantitative methods.- In the second part of the dissertation, we extend the characterization of weak normalization in the pure lambda-calculus to an infinitary lambda-calculus narrowly related to Böhm trees, which was introduced by Klop et al. This gives a positive answer to a question known as Klop's problem. In that purpose, it is necessary to simultaneously introduce a system (system S) featuring infinite types and resorting to an intersection operator that we call sequential, and a validity criterion in order to discard unsound proofs that coinductive grammars give rise to. This also allows us to give a solution to TLCA problem #20 (type-theoretic characterization of hereditary permutations). It is to be noted that those two problem do not have a solution in the finite case (Tatsuta, 2007).- Finally, we study the expressive power of coinductive type grammars, without any validity criterion. We must once more resort to system S and we show that every term is typable in a non-trivial way with infinite types and that one can extract semantical information from those typings e.g. the order (arity) of any lambda-term. This leads us to introduce a method that allows typing totally unproductive terms (the so-called mute terms), which is inspired from first order logic. This result establishes that, in the coinductive extension of the relational model, every term has a non-empty interpretation. Using a similar method, we also prove that system S surjectively collapses on the set of points of this model

This work contains students' communication analysis, the design of new information system for students and its implementation. New system integrates the social network Facebook, the Google Docs and the Google Calendar. The result of this master's thesis is working system written in Java language. The system is based on the students' communication analysis and the requirements of the Students' Union.

This master's thesis deals with analysis of user's typing skills in Windows system. Touch method technique for fast keyboard typing is described. The possibilities of Windows keyboard hooking and GUI making are mentioned. The description of segmentation of written text and writing level evaluation techniques are part of this thesis. Another part deals with the system implementation. The result application collects data about user's typing skills and evaluates the quality of typing and number of mistakes.

Die Optimierung der Anordnung von Objekten ist eine alte Herausforderung in der Wirtschaft. Anwendungsfälle erstrecken sich von der Stauraumoptimierung bei der Beladung von Lkws, Schiffen und Flugzeugen in der Logistik über die Packungsoptimierung bis zur Zuschnittoptimierung in den metall-, textil- und holzverarbeitenden Industrien. Die große Spanne an Szenarien und Randbedingungen erfordert jeweils angepasste Lösungsalgorithmen. Mit den neuen Herstellungstechnologien des Rapid Prototyping (zum Beispiel 3D-Druck oder Lasersintering), erlangt eine neue Ausprägung des Problemraums wirtschaftliche Bedeutung. Zur Lösung des Problems, soll untersucht werden, inwieweit sich etablierte Algorithmen der Stauraum- und Packungsoptimierung an die neuen Randbedingungen anpassen lassen und ob sich Algorithmen zur Zuschnittoptimierung in die dritte Dimension übertragen lassen.

In der vorliegenden Studie wurde die Sanierung einer durch S. aureus verursachten Eutergesundheitsstörung in einem hessischen Milchviehbestand mittels klassischer Sanierungsmaßnahmen über einen Zeitraum von 18 Monaten begleitet. Durch konsequente Einhaltung der Sanierungsmaßnahmen nach dem Fünf-Punkte-Plan und die räumliche Trennung der Herde in eine S. aureus-positive und -negative Gruppe sank die S. aureus-Prävalenz im Betrieb innerhalb von 15 Monaten von 30% auf <1%. Nach 18 Monaten waren erstmalig keine Neuinfektionen mehr mit S. aureus zu verzeichnen. Zusätzlich zu den im Abstand von drei Monaten durchgeführten Viertelanfangsgemelk (VAG)- Gesamtbestandsuntersuchungen wurden Umweltproben bakteriologisch auf das Vorhandensein von S. aureus untersucht. Diese Untersuchungen verliefen ausschließlich mit negativem Ergebnis. Die im Untersuchungszeitraum asservierten 218 S. aureus-Isolate aus diesem Betrieb wurden genotypisch mittels PCR untersucht. Thermonuklease-Gen, Protein A-Gen (IgG-bindende Region) und Polymorphismen bei Protein A-Gen (Xr-Region) sowie Koagulase-Gen ermöglichten die Unterscheidung in sechs Typen. Zusätzlich wurden 80 dieser Isolate mittels Pulsfeldgelelektrophorese (Pfge, Gold Standard) typisiert. Es konnten zwei Pfge-Typen gefunden werden: Pfge-Typ I mit insgesamt 10 Subtypen (bei 78 Isolaten) und Pfge-Typ II (bei zwei Isolaten). Der Pfge-Typ II wurde ausschließlich bei einem Zukaufstier nachgewiesen, das vor der Einstallung in diesen Betrieb nicht zytobakteriologisch untersucht worden war. Die 12 unterschiedlichen Pfge-Typen bzw. -Subtypen wurden zusätzlich mittels Staphylokokken-Protein A- (spa)-Typisierung untersucht. Dabei zeigte sich, dass alle Subtypen des Pfge-Typs I dem spa-Typ t2067 zugeordnet werden konnten und der Pfge-Typ II dem spa-Typ t2112 entsprach. 92 weitere bovine S. aureus-Mastitisisolate wurden möglichst randomisiert über das Landesgebiet Hessens entnommen und mittels dieser Typisierungsmethode untersucht. Die Isolate stammten ebenfalls aus S. aureus-Problembetrieben und wurden aus VAG von (sub-) klinischen Mastitiden in Reinkultur isoliert. Insgesamt konnten 28 spa-Typen unterschieden werden. Durch den Algorithmus BURP wurden 57 dieser Isolate dem Clonal Complex CC543 zugeordnet und waren demnach genetisch eng miteinander verwandt. Der in dem Sanierungsbetrieb vorherrschende spa-Typ t2067 war dem CC543 nicht zuzuordnen. Die Anwendung der spa-Typisierung in der Routinediagnostik und damit die Möglichkeit der laborübergreifenden, möglichst zentralisierten Datendokumentation der Ergebnisse könnten zukünftig die Identifizierung besonders häufig vorkommender und damit hochkontagiöser S. aureus-Stämme ermöglichen.

L’objectif de ces travaux de thèse a été de contribuer à la compréhension de la physiopathologie des infections sur matériel ostéo-articulaire (IMOA) à C. acnes. Dans un premier temps, nous avons typé par MLST 108 isolats de C. acnes responsables de 34 cas d’IMOAs monomicrobiennes et corrélé les résultats de typage aux données clinico-biologiques. Nous avons ainsi montré que les IMOAs à C. acnes correspondent à 2 entités cliniques : i) les cas « homotypiques » qui sont des vraies infections dues à un clone de C. acnes responsable d’une réponse inflammatoire de l’hôte ii) les cas hétérotypiques qui sont une colonisation ou contamination itérative du matériel ostéo-articulaire en l’absence de réponse inflammatoire de l’hôte. Ces données de typage ont souligné les limites de la définition microbiologique actuelle d’une IMOA quand il s’agit de C. acnes et la nécessité d’intégrer un outil moléculaire fiable dans le diagnostic microbiologique de routine de ces infections. Nous avons par conséquent évalué la technique SLST développée pour un typage rapide et optimal de C. acnes en routine. Le pouvoir discriminant de cette technique était insuffisant suggérant que seule la mise en place du NGS en temps réel dans les laboratoires de microbiologie pourrait répondre au besoin de typage moléculaire pour améliorer le diagnostic microbiologique de ces infections.Nos résultats de typage ont montré que la clonalité de l’infection plutôt que le complexe clonal (CC) est le principal facteur déterminant du processus physiopathologique et inflammatoire de l’IMOA à C. acnes. Cette conclusion est concordante avec les résultats que nous avons obtenus dans un modèle in vitro d’infection de macrophages THP-1 par C. acnes. Grâce à ce modèle, nous avons pu montrer que la réponse inflammatoire in vitro de nos isolats est souche –et non CC– dépendante. De plus, les réponses inflammatoires in vitro et in vivo n’étaient pas corrélées. Ceci souligne les limites des modèles in vitro dans l’étude de la physiopathologie des IMOAs à C. acnes dans lesquels l’adaptation de la bactérie à l’hôte est complètement négligée lors de l’étude de la réponse immune. Dans la dernière partie de ce travail, nous avons confirmé l’importance de l’environnement dans le conditionnement du comportement de la bactérie. Nous avons mené une étude comparative des caractéristiques culturales ex vivo et ex vitro de nos isolats de C. acnes. Nous avons montré l’impact du CC et des conditions environnementales, par extension la pression que peut exercer l’hôte, sur le profil cultural de C. acnes. En conclusion, nos travaux montrent qu’une approche multifactorielle, intégrant à la fois la génomique et la réponse de l’hôte, est nécessaire pour comprendre la physiopathologie des IMOAs à C. acnes. / The aim of this thesis was to contribute to the understanding of the physiopathology of C. acnes orthopedic-device related infections (ODRI). Firstly, we typed by MLST 108 C. acnes isolates responsible for 34 cases of monomicrobial ODRIs and correlated typing results with bio-clinical data. We have shown that C. acnes ODRIs correspond to two clinical entities: i) "homotypic" cases corresponding to true infections with a single pathogenic clone of C. acnes eliciting an inflammatory response ii) heterotypic cases corresponding to colonization or iterative contamination of the implant without systemic inflammatory response. These typing data highlighted the limitations of the current microbiological definition of ODRI when it comes to C. acnes and the need to incorporate a reliable molecular tool into the routine microbiological diagnosis of these infections. We therefore evaluated the SLST technique developed for a rapid and optimal typing of C. acnes. The discriminating power of this technique was insufficient suggesting that only the establishment of real-time NGS in microbiology laboratories could improve the microbiological diagnosis. Our typing results showed that the clonal status of the infection and not CC is the main determining factor in the physiopathological and inflammatory process of C. acnes ODRI. This conclusion is consistent with our results obtained on an in vitro model of a macrophage THP-1 infection. Using this model, we have shown that the in vitro inflammatory response of our isolates is strain- and non-CC-dependent. In addition, the in vitro and in vivo inflammatory responses were not correlated. This underscores the limitations of in vitro models in the study of C. acnes ODRIs in which the adaptation of the bacteria to the host is completely neglected during the study of the immune response. Finally, we confirmed the importance of the environment in the conditioning of the behavior of the bacterium. We conducted a comparative study of the ex vivo and ex vitro growth characteristics of our C.acnes isolates. We have shown the impact of CC and environmental conditions, by extension the pressure that can exert the host, on the cultural profile of C. acnes. In conclusion, our work shows that a multifactorial approach, integrating both genomics and host response, is needed to understand the physiopathology of C. acnes ODRI.

No description available.

[pt] Linguagens dinamicamente tipadas, tais como Lua, não usam tipos estáticos em favor de simplicidade e exibilidade, porque a ausência de tipos estáticos significa que programadores não precisam se preocupar em abstrair tipos que devem ser validados por um verificador de tipos. Por outro lado, linguagens estaticamente tipadas ajudam na detecção prévia de diversos bugs e também ajudam na estruturação de programas grandes. Tais pontos geralmente são vistos como duas vantagens que levam programadores a migrar de uma linguagem dinamicamente tipada para uma linguagem estaticamente tipada, quando os pequenos scripts deles evoluem para programas complexos. Sistemas de tipos opcionais nos permitem combinar tipagem dinâmica e estática na mesma linguagem, sem afetar a semântica original da linguagem, tornando mais fácil a evolução de código tipado dinamicamente para código tipado estaticamente. Desenvolver um sistema de tipos opcional para uma linguagem dinamicamente tipada é uma tarefa desafiadora, pois ele deve ser o mais natural possível para os programadores que já estão familiarizados com essa linguagem. Neste trabalho nós apresentamos e formalizamos Typed Lua, um sistema de tipos opcional para Lua, o qual introduz novas características para tipar estaticamente alguns idiomas e características de Lua. Embora Lua compartilhe várias características com outras linguagens dinamicamente tipadas, em particular JavaScript, Lua também possui várias características não usuais, as quais não estão presentes nos sistemas de tipos dessas linguagens. Essas características incluem funções com aridade flexível, atribuições múltiplas, funções que são sobrecarregadas no número de valores de retorno e a evolução incremental de registros e objetos. Nós discutimos como Typed Lua tipa estaticamente essas características e também discutimos nossas decisões de projeto. Finalmente, apresentamos uma avaliação de resultados, a qual obtivemos ao usar Typed Lua para tipar código Lua existente. / [en] Dynamically typed languages such as Lua avoid static types in favor of simplicity and exibility, because the absence of static types means that programmers do not need to bother with abstracting types that should be validated by a type checker. In contrast, statically typed languages provide the early detection of many bugs, and a better framework for structuring large programs. These are two advantages of static typing that may lead programmers to migrate from a dynamically typed to a statically typed language, when their simple scripts evolve into complex programs. Optional type systems allow combining dynamic and static typing in the same language, without affecting its original semantics, making easier this code evolution from dynamic to static typing. Designing an optional type system for a dynamically typed language is challenging, as it should feel natural to programmers that are already familiar with this language. In this work we present and formalize the design of Typed Lua, an optional type system for Lua that introduces novel features to statically type check some Lua idioms and features. Even though Lua shares several characteristics with other dynamically typed languages such as JavaScript, Lua also has several unusual features that are not present in the type system of these languages. These features include functions with exible arity, multiple assignment, functions that are overloaded on the number of return values, and the incremental evolution of record and object types. We discuss how Typed Lua handles these features and our design decisions. Finally, we present the evaluation results that we achieved while using Typed Lua to type existing Lua code.

No description available.

The problem of this study was to make a comparative analysis of the methods and factors employed in grading students in physical education, typing, and English in fifty Class "A" high schools of Texas for the school year of 1949-59. This analysis was of two pars. One phase gave consideration to various methods used in grading pupils. The other considered factors that go to make the whole of student grades and the percentage attached to each factor. The two phases were so interrelated that it was felt that this study would not be complete without the inclusion of both.