Le $\lambda \mu^{\wedge \vee}$-calcul est une extension du $\lambda$-calcul associée à la déduction naturelle classique où sont considérés tous les connecteurs.<br>Les principaux résultats de cette thèse sont :<br>- La standardisation, la confluence et une extension de la machin de J.-L. Krivine en $\lambda \mu^{\wedge \vee}$-calcul.<br>- Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures.<br>- Une sémantique de réalisabilité pour le $\lambda \mu^{\wedge \vee}$-calcul qui permet de caractériser le comportement calculatoire de certains termes typés et clos.<br>- Un théorème de complétude pour le $\lambda \mu$-calcul simplement typé.<br>- Une introduction à un $\lambda \mu^{\wedge \vee}$-calcul par valeur confluent.

Le multilinguisme arabe-latin que nous qualifions de multilinguisme lourd, présente deux particularités fondamentales qui le distinguent du multilinguisme souple (même famille linguistique) : la représentation et la bidirectionnalité graphiques ou textuelles.<br /><br />Le mécanisme de la représentation et du traitement des caractères et de leurs soubassements de codage et de normalisation constituent encore un point contraignant à la transparence linguistique des systèmes et des interfaces homme-machines multilingues. Si le problème est partiellement résolu sur les plates-formes monopostes et locales, les systèmes d'information scientifique et technique ouverts et distribués (i.e. Internet) sont encore soumis à l'hégémonie linguistique latine et plus particulièrement anglo-saxonne. L'introduction de la langue arabe (et autres non latines) y est certes en progression, mais elle reste encore interdite aux zones systèmes (URIs, protocoles, systèmes opératoires... ). Notre contribution à l'i18n et la l10n des systèmes d'information multilingues en général et les interfaces Homme-Machine en particulier prend forme d'une proposition qui part du principe de correspondance entre un mécanisme numérique et un jeu de caractères unifiés (Unicode, ISO 10464).<br /><br />La bidirectionnalité est aussi un facteur de contrainte qui pèse sur les interfaces multilingues homme-machine. Les algorithmes de tri, les méthodes des traitements logiques et visuels des incises et des bris, les techniques de l'étiquetage et de la négociation linguistiques entre systèmes distribués, l'opposition entre la rigueur gauche-droite des chiffres et leur traitement algorithmique de droite à gauche constituent les points les plus importants de notre étude du mécanisme Bidi. <br /><br />Notre objectif essentiel est la révocation des systèmes d'information et de communication multilingue hérités pour ouvrir d'autres pistes de recherche dans les domaines de l'industrie de la langue et de la sociolinguistique.

<p>Abstract</p><p>Purpose/Aim: The aim is to investigate if there are any differences in the reporting from the Olympic games and the Paralympic games, according to different periodicals or magazines, with focus on Paralymics and sports for handicapped. If so, what are those differences?</p><p>Material/Method: The material consists of two periodicals, or magazines; Svensk idrott which is the official paper for the swedish Riksidrottsförbundet, and Handikappidrott, which is the official paper for the swedish Handikappidrottsförbundet. Articles considering the summer games in 1972 and 1976, 1984, 1996 and 2000 was studied with regard to models developed by Algirdas J. Greimas. The methods are both quantitative and qualitative.</p><p>Main results: The main results are that the biggest difference between the periodicals really lie in the selection of articles and also in the amount of articles published, considering the games. In Handikappidrott, the articles are aimed towards an initiated audience who are supposed to know much about handicapped people and their sports. Svensk idrott focuses a lot more on different aspects of the Olympic games, such as politics and economy. Also has the aspect of normalisation been of current interest – the problem is that the more of handicapped people and issues that are presented to the audience in order to pinpoint the normality of the issue, the more focus come to lie on what is different from the non-handicapped, and in that way enlarge the gap between handicapped an non-handicapped.</p><p>Keywords: Olympic games, Paralympics, actants, narrator, implied author, normalisation</p>

Abstract Purpose/Aim: The aim is to investigate if there are any differences in the reporting from the Olympic games and the Paralympic games, according to different periodicals or magazines, with focus on Paralymics and sports for handicapped. If so, what are those differences? Material/Method: The material consists of two periodicals, or magazines; Svensk idrott which is the official paper for the swedish Riksidrottsförbundet, and Handikappidrott, which is the official paper for the swedish Handikappidrottsförbundet. Articles considering the summer games in 1972 and 1976, 1984, 1996 and 2000 was studied with regard to models developed by Algirdas J. Greimas. The methods are both quantitative and qualitative. Main results: The main results are that the biggest difference between the periodicals really lie in the selection of articles and also in the amount of articles published, considering the games. In Handikappidrott, the articles are aimed towards an initiated audience who are supposed to know much about handicapped people and their sports. Svensk idrott focuses a lot more on different aspects of the Olympic games, such as politics and economy. Also has the aspect of normalisation been of current interest – the problem is that the more of handicapped people and issues that are presented to the audience in order to pinpoint the normality of the issue, the more focus come to lie on what is different from the non-handicapped, and in that way enlarge the gap between handicapped an non-handicapped. Keywords: Olympic games, Paralympics, actants, narrator, implied author, normalisation

European cities are becoming increasingly multicultural and diverse in terms of lifestyles and socioeconomic conditions. However, in planning for sustainable urban development, implications of this increased diversity and possibly conflicting perspectives are seldom considered. The aim of this thesis is to explore dimensions of justice and politics in sustainable urban development by studying inclusionary/exclusionary effects of discursive power of official strategies for eco-friendly living on the one hand and everyday lifestyles on the other, in ethnically and socially diverse areas. Two case studies have been conducted, one in a city district of Stockholm, Sweden, and one in an area of Sheffield, England. The empirical material consists of interviews with residents, interviews with planners and officials and an analysis of strategic planning documents. The case study in Stockholm illustrated the prevalence of a dominant discourse among residents in which Swedishness is connected with environmental responsibility in the form of tidiness, recycling and familiarity with nature. In Sheffield there are more competing and parallel environmental discourses. The mainstream British environmental discourse and sustainability strategies are being criticised from Muslim as well as green radical perspectives. The mainstream discourse is criticised for being tokenistic in its focus on gardening, tidiness, recycling and eco-consumption, and hence ignoring deeper unsustainable societal structures. This can be interpreted as a postpolitical condition, in which there is a consensus around “what needs to be done,” such as more recycling, but in which difficult societal problems and conflicting perspectives on these are not highlighted. In the thesis it is argued that the strategies for urban sustainability are underpinned by Swedish/British middle-class norms, entailing processes of (self-)disciplining and normalisation of the Other into well-behaving citizens. It is argued that an appreciation of the multiple and others’ ways of saving natural resources would make the sustainability strategies more attuned to social and cultural diversity as well as more environmentally progressive. Finally, the importance of asserting the political in sustainability strategies is stressed, highlighting the organisation of society and possible alternative socioenvironmental futures. / QC 20100421

Depuis 2010, le gouvernement canadien a créé une loi qui exige 5% de biocarburant dans l’essence, et ce, dans un contexte d’insécurité alimentaire dont souffrent les plus défavorisés. Cette thèse fait l’analyse critique du discours des organisations privées qui ont promu les biocarburants dans ce contexte. Comment en sont-ils arrivés à fabriquer la normalité de l’usage des biocarburants? Cette dernière se produit par la mise en valeur de nouveaux emplois dans l’industrie, la promotion d’une économie rurale vigoureuse, la présentation de l’État comme facilitateur des marchés ainsi que l’accent mis sur les impacts environnementaux favorables des biocarburants. La normalisation s’explique aussi par la dénaturation des grains et la radicalisation du rôle du fermier afin que ceux-ci concordent avec l’idéologie (néo)libérale. Il importe que la criminologie critique, se positionne au sein d’une zémiologie, dont les objets d’études portent sur les torts sociaux émanant des structures et l’organisation inégalitaire de nos sociétés.

La capacité de production de la parole est apprise et maintenue au moyen d'une boucle de perception-action qui permet aux locuteurs de corriger leur propre production en fonction du retour perceptif reçu. Ce retour est auditif et proprioceptif, mais pas visuel. Ainsi, les sons de parole peuvent être complétés par l'affichage des articulateurs sur l'écran de l'ordinateur, y compris ceux qui sont habituellement cachés tels que la langue ou le voile du palais, ce qui constitue de la parole augmentée. Ce type de système a des applications dans des domaines tels que l'orthophonie, la correction phonétique et l'acquisition du langage. Ce travail a été mené dans le cadre du développement d'un système de retour articulatoire visuel, basé sur la morphologie et les stratégies articulatoires d'un locuteur de référence, qui anime automatiquement une tête parlante 3D à partir du son de la parole. La motivation de cette recherche était d'adapter ce système à plusieurs locuteurs. Ainsi, le double objectif de cette thèse était d'acquérir des connaissances sur la variabilité inter-locuteur, et de proposer des modèles pour adapter un clone de référence, composé de modèles des articulateurs de la parole (lèvres, langue, voile du palais, etc.), à d'autres locuteurs qui peuvent avoir des morphologies et des stratégies articulatoires différentes. Afin de construire des modèles articulatoires pour différents contours du conduit vocal, nous avons d'abord acquis des données qui couvrent l'espace articulatoire dans la langue française. Des Images médio-sagittales obtenues par Résonance Magnétique (IRM) pour onze locuteurs francophones prononçant 63 articulations ont été recueillis. L'un des principaux apports de cette étude est une base de données plus détaillée et plus grande que celles disponibles dans la littérature. Cette base contient, pour plusieurs locuteurs, les tracés de tous les articulateurs du conduit vocal, pour les voyelles et les consonnes, alors que les études précédentes dans la littérature sont principalement basées sur les voyelles. Les contours du conduit vocal visibles dans l'IRM ont été tracés à la main en suivant le même protocole pour tous les locuteurs. Afin d'acquérir de la connaissance sur la variabilité inter-locuteur, nous avons caractérisé nos locuteurs en termes des stratégies articulatoires des différents articulateurs tels que la langue, les lèvres et le voile du palais. Nous avons constaté que chaque locuteur a sa propre stratégie pour produire des sons qui sont considérées comme équivalents du point de vue de la communication parlée. La variabilité de la langue, des lèvres et du voile du palais a été décomposé en une série de mouvements principaux par moyen d'une analyse en composantes principales (ACP). Nous avons remarqué que ces mouvements sont effectués dans des proportions différentes en fonction du locuteur. Par exemple, pour un déplacement donné de la mâchoire, la langue peut globalement se déplacer dans une proportion qui dépend du locuteur. Nous avons également remarqué que la protrusion, l'ouverture des lèvres, l'influence du mouvement de la mâchoire sur les lèvres, et la stratégie articulatoire du voile du palais peuvent également varier en fonction du locuteur. Par exemple, certains locuteurs replient le voile du palais contre la langue pour produire la consonne /ʁ/. Ces résultats constituent également une contribution importante à la connaissance de la variabilité inter-locuteur dans la production de la parole. Afin d'extraire un ensemble de patrons articulatoires communs à différents locuteurs dans la production de la parole (normalisation), nous avons basé notre approche sur des modèles linéaires construits à partir de données articulatoires. Des méthodes de décomposition linéaire multiple ont été appliquées aux contours de la langue, des lèvres et du voile du palais. L'évaluation de nos modèles repose sur deux critères: l'explication de la variance et l'erreur quadratique moyenne. Les modèles ont également été évalués en utilisant une procédure de validation croisée. Le but de l'utilisation de telle procédure était de vérifier la capacité de généralisation des modèles en évaluant leurs performances sur des données qui n'ont pas été utilisées pour leur construction. Afin de modéliser la langue, les lèvres et le voile du palais avec un ensemble commun de composantes pour tous les locuteurs, plusieurs méthodes de décomposition linéaires multiple ont été utilisées et comparées. L'ACP conjointe a donné les meilleurs résultats. En conclusion, nous avons constaté une réduction considérable en termes de nombre de composantes nécessaires lors de l'utilisation d'ACP conjointe, par rapport au nombre total de composantes nécessaires par les modèles ACP individuels de tous les locuteurs. Ces résultats de modélisation constituent une extension importante des études disponibles dans la littérature, à des locuteurs plus nombreux, incluant de plus nombreuses articulations (en particulier les consonnes) et de plus nombreux articulateurs (lèvres, voile du palais).

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.

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.

Cette thèse traite de la reconnaissance des formes dans les images numériques. Une représentation appropriée des formes est déduite de l'analyse des perturbations qui n'affectent pas la reconnaissance : changement de contraste, occlusion partielle, bruit, perspective. Les atomes de cette représentation, appelés "éléments de forme", fournissent des descriptions semi-locales des formes. L'appariement de ces éléments permet de reconnaitre des formes partielles. Les formes globales sont alors définies comme des groupes de formes partielles présentant une cohérence dans leur disposition spatiale. L'aspect fondamental de ce travail est la mise en place de seuils non-supervisés, à tous les niveaux de décision du processus de reconnaissance. Nous proposons des règles de décision pour la en correcpondance de formes partielles ainsi que pour la détection de formes globales. Le cadre proposé est basé sur une méthodologie générale de la détection dans laquelle un événement est significatif s'il n'est pas susceptible d'arriver par hasard.