La tournée africaine du général de Gaulle, effectuée du 20 au 27 août 1958, la veille du référendum constitutionnel de septembre qui était tenu dans la Métropole et dans les colonies, n'avait jusqu'ici fait l'objet d’aucune étude systématique. Plusieurs historiens, politiciens ou administrateurs des colonies et autres, ont évoqué ce voyage, mais toujours dans le cadre d'une étude générale qui porte le grand titre ambigu" de "décolonisation de l'Afrique noire". Mais aucun n'a fait ressortir le but réel de cette tournée, qui, loin de revêtir un aspect émancipateur comme on l'a toujours pensé, va plutôt permettre à de Gaulle et aux gouvernants français, grâce â une domestication en apparence librement consentie, de perpétuer le pacte colonial aux seules colonies qui restaient a la France en 1958: celles de l'Afrique noire. Cette année (1958) est une période très troublée en France à cause de la crise franco-algérienne qui est à son paroxysme et d'une manière indirecte va influencer la "nouvelle" politique française en Afrique noire. Cette crise algérienne marque aussi le grand tournant de la f i n de la IVe république et donne naissance à la Ve avec le retour de de Gaulle. La suite logique des crises coloniales étant devenue un tourment aux yeux des gouvernants français, la probabilité de voir l'Afrique noire, dernière chance de la survie du colonialisme français, prendre la relève de l'Algérie dans ces conflits coloniaux, était déjà perçue dès 1957. L'utilisation de la presse, constituée ici par le Monde, le Figaro, l'Aurore et l'Humanité, comme source de base était primordiale. En effet les quotidiens sont les documents les plus adéquats pour étudier la perception d'un événement par l’opinion publique, surtout que cette presse sélectionnée présente l'opinion des diverses couches socio-politiques impliquées ou qui subissent ces événements. Plus encore ces mêmes quotidiens ont permis à de Gaulle et son groupe de manipuler l'opinion publique française, africaine et même internationale, ceci pour atteindre leur but qui est en fait la relance du colonialisme français, synonyme de grandeur de la France. Une grandeur qui, pour les gouvernants français, est inéluctablement liée à l'existence de colonies françaises. Ainsi soula couverture d'une mission "civilisatrice" non périmée, les gouvernants français s'adressant aux Africains, vont p~6ner une politique dite de renouveau, dont la toile de fond reste cependant la même: la conservation des colonies africaines dans le giron français. / Québec Université Laval, Bibliothèque 2013

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.

Cette thèse traite de la theorie de la preuve pour les logiques a points fixes, telles que le μ-calcul, lalogique lineaire a points fixes, etc. ces logiques sont souvent munies de systèmes de preuves finitairesavec des règles d’induction à la Park. Il existe néanmoins d’autres sytèmes de preuves pour leslogiques à points fixes, qui reposent sur la notion de preuve infinitaire, mais qui sont beaucoupmoins developpés dans la litterature. L’objectif de cette thèse est de pallier à cette lacune dansl’état de l’art, en developpant la théorie de la preuve infnitaire pour les logiques a points fixes,avec deux domaines d’application en vue: les langages de programmation avec types de données(co)inductifs et la vérification des systèmes réactifs.Cette thèse contient trois partie. Dans la première, on rappelle les deux principales approchespour obtenir des systèmes de preuves pour les logiques à points fixes: les systèmes finitaires avecrègle explicite d’induction et les systèmes finitaires, puis on montre comment les deux approchesse relient. Dans la deuxième partie, on argumente que les preuves infinitaires ont effectivement unréel statut preuve-theorique, en montrant que la logique lineaire additive multiplicative avec pointsfixes admet les propriétés d’élimination des coupures et de focalisation. Dans la troisième partie,on utilise nos developpements sur les preuves infinitaires pour monter de manière constructive lacomplétude du μ-calcul lineaire relativement à l’axiomatisation de Kozen. / The subject of this thesis is the proof theory of logics with fixed points, such as the μ-calculus,linear-logic with fixed points, etc. These logics are usually equipped with finitary deductive systemsthat rely on Park’s rules for induction. other proof systems for these logics exist, which relyon infinitary proofs, but they are much less developped. This thesis contributes to reduce thisdeficiency by developing the infinitary proof-theory of logics with fixed points, with two domainsof application in mind: programming languages with (co)inductive data types and verification ofreactive systems.This thesis contains three parts. In the first part, we recall the two main approaches to theproof theory for logics with fixed points: the finitary and the infinitary one, then we show theirrelationships. In the second part, we argue that infinitary proofs have a true proof-theoreticalstatus by showing that the multiplicative additive linear-logic with fixed points admits focalizationand cut-elimination. In the third part, we apply our proof-theoretical investigations to obtain aconstructive proof of completeness for the linear-time μ-calculus w.r.t. Kozen’s axiomatization.

L'enclavement des territoires de la Politique de la ville fait l'objet d'un débat. D'un côté, l'image des zones urbaines sensibles comme enclavées est forte dans les discours sur la ville et dans les représentations collectives. D'un autre côté, cet enclavement est nuancé, voire réfuté, par de nombreux chercheurs qui suggèrent de se concentrer sur les facteurs socio-économique de l'exclusion de leurs habitants. Positionnée à « l’entre-deux » entre sciences humaines et sociales et géomatique, cette thèse élabore une méthode générique de mesure de l'enclavement dans les espaces urbains à l'aide d'un système d'information géographique. Nous questionnons ainsi l'apport de la géomatique à une problématique relevant jusque-là de disciplines comme la géographie, la sociologie ou l'urbanisme. Nous entendons l'enclavement comme une situation de faible potentiel de contact avec l'altérité, qui réduit les échanges entre une entité et le reste du territoire, et provoque une mise à l'écart de ses habitants. Nous proposons de distinguer trois dimensions de l'enclavement : la Fermeture, l'Isolement et la Différenciation. Ces trois dimensions structurent notre méthode. Chacune renvoie à des axes de recherche différents – les coupures urbaines, les mobilités piétonnes, la caractérisation de la forme urbaine, l'accessibilité, la mesure de ségrégation – que nous mobilisons pour construire des indicateurs géographiques d'enclavement. Nous appliquons ensuite cette méthode aux zones urbaines sensibles. Cette application spécifique nous permet à la fois de valider notre méthode, en recoupant des résultats connus avec d'autres approches (urbanisme, sociologie), et à la fois de contribuer au débat sur l'enclavement des territoires de la Politique de la ville au moyen d'une approche quantitative / In France, there is a debate in Urban Policies: are the “zones urbaines sensibles”, underprivileged urban areas benefiting from specific public policies, suffering from geographical isolation ? On the one hand, these areas are perceived in collective representations as “enclaves” where inhabitants are blocked in their district. On the other hand, this isolation is nuanced, even refuted, by many researchers who suggest focusing on the socio-economic factors of exclusion.With an approach in between social sciences and geomatics, this PhD thesis develops a generic method of measuring geographical isolation in urban spaces by using a geographic information system. We aims to question the contribution of geomatics to a debate that until then belong to disciplines such as geography, sociology or planning.We define geographical isolation as a situation of weak potential for contact with otherness, which reduces the exchanges between an entity and the rest of the territory, and causes the severance of its inhabitants. We propose to distinguish three dimensions of geographical isolation: Enclosing, Remoteness and Differentiation. These three dimensions give a frame to our method. Each refers to different fields of research – “community severance” or “barrier effect”, pedestrian mobility, characterization of urban form, accessibility, segregation measure – that we mobilize to construct indicators of geographical isolation.We then apply this method to the “zones urbaines sensibles”. This specific application enables us both to validate our method, by combining known results with other approaches (planning, sociology), and both to contribute to the debate on the geographical isolation of the “zones urbaines sensibles” with a quantitative approach

L'exposition des polymères aux contraintes de leur environnement d'usage provoque une modification de la structure chimique des macromolécules qui se traduit par une évolution irréversible de leurs propriétés fonctionnelles. L'objectif majeur de cette thèse était de passer, dans la compréhension des phénomènes de photovieillissement, du niveau moléculaire au niveau macroscopique. Pour ce faire, trois polymères dont le vieillissement est gouverné par des réactions de réticulation et / ou de coupures de chaîne, ont été étudiés. Nous avons principalement développé l'utilisation de la microscopie à force atomique en effectuant des nanoindentations tant à la surface que dans l'épaisseur du matériau irradié et comparé les résultats à de nombreuses autres techniques. Cette méthodologie nous a permis de progresser dans la connaissance des relations qui existent entre modification de la structure chimique et variation des propriétés physiques de polymères sous l'impact du photovieillissement.

Dans cette thèse on s'intéresse aux formes de "circularité" qui apparaissent dans la théorie de la preuve de la logique du second ordre et de son contrepartie constructive, le Système F.Ces "circularités", ou "cercles vicieux" (Poincaré 1900), sont analysées sur la base d'une distinction entre deux points de vue distincts et irréductible (à cause des théorèmes d'incomplétude): le premier ("le pourquoi", Girard 1989) concerne la cohérence et l'Hauptsatz et demande des méthodes infinitaires (i.e. non élémentaires) de preuve. Le deuxième ("le comment", Girard 1989) concerne le contenu computationnel et combinatoire des preuves, donné par la correspondance entre preuves et programmes, et ne demande que de méthodes élémentaires de preuve.Dans la première partie de la thèse, dévouée au "pourquoi", les arguments philosophiques traditionnels sur les "cercles vicieux" sont confrontés avec la perspective qui émerge de la démonstration de l' Hauptsatz pour la logique de second ordre (obtenue par Girard avec la technique des candidats de réductibilité).Dans la deuxième partie de la thèse, dévouée au "comment", deux approches combinatoires aux cercles vicieux sont proposés: la première se basant sur la théorie du polymorphisme paramétrique, la deuxième sur l'analyse géométrique du typage qui vient de la théorie de l'unification. / In this dissertation several issues concerning the proof-theory of second order logic and its constructive counterpart (System F, Girard 1971) are addressed. The leitmotiv of the investigations here presented is the apparent "circularity'' or "impredicativity'' of second order proofs. This circularity is reflected in System F by the possibility to type functions applied to themselves, in contrast with Russell's idea that typing should rather forbid such ``vicious circles'' (Poincare 1906). A fundamental methodological distinction between two irreducible (because of incompleteness) approaches in proof theory constitutes the background of this work: on the one hand, "why-proof theory'' ("le pourquoi'', Girard 1989) addresses coherence and the Hauptsatz and requires non-elementary ("infinitary'') techniques; on the other hand, "how-proof theory'' ("le comment'', Girard 1989) addresses the combinatorial and computational content of proofs, given by the correspondence between proofs and programs, and is developed on the basis of elementary ("finitary'') techniques. }In the first part of the thesis, dedicated to "why-proof theory'', the traditional philosophical arguments on "vicious circles'' are confronted with the perspective arising from the proof of the Hauptsatz for second order logic (first obtained in Girard 1971 with the technique of reducibility candidates).In the second part of the thesis, dedicated to "how-proof theory'', two combinatorial approaches to "vicious circles'' are presented, with some technical results: the first one based on the theory of parametric polymorphism, the second one on the geometrical analysis of typing coming from unification theory.

L’activité de personnalisation d’albums-souvenirs, communément appelée le scrapbooking, découle d’une pratique coutumière de création d’archives personnelles et familiales. Aujourd’hui, au Québec comme ailleurs, cette pratique se perpétue et se renouvelle dans la tradition d’un art d’assemblage et de collage de matériaux divers, où les photographies de familles ont une place prépondérante. Devant les frontières qui s’estompent entre les divertissements, la culture et les pratiques traditionnelles, on est droit de se questionner sur l’examen que soumet l’ethnologie à ces récentes activités de loisirs qui font l’objet d’engouement. Ce mémoire documente sous ses principales facettes la pratique actuelle de scrapbooking présente au Québec. À sa manière, il pose un regard sur la manière dont les composantes des loisirs d’aujourd’hui influencent la création et la transmission du patrimoine familial. Comment les albums personnalisés d’aujourd’hui s’inscrivent-ils dans les mécanismes de création des héritages familiaux? L’étude s’appuie un travail d’enquête ethnologique de terrain dans l’agglomération de la ville de Québec. L'enquête orale auprès d’amatrices de cette activité a permis d’une part, d’acquérir des connaissances sur cette production et d’autre part, d’étudier le discours des adeptes de ce loisir. De façon plus spécifique, nous nous sommes attardée aux facettes suivantes : la logistique de l’activité dans sa dimension créative et identitaire, le scrapbook qui en résulte, les contextes de performance de l’activité et leur influence sur les processus de création du scrapbook. Finalement, nous avons exposé le rôle que le scrapbooking joue dans le patrimoine familial des amatrices. En tant que pratique d’amateurs, l’activité actuelle de scrapbooking est située en marge des pratiques artistiques traditionnelles en raison du renouvellement de sa forme d’expression. Elle fait l’objet de plusieurs enjeux actuels reliés entre autres, aux produits de consommation de masse et aux nouvelles technologies de l’information. / The activity of album personalisation – most often called scrapbooking – results from the customary practice of personal or familial archive creation. Today – in Quebec and elsewhere – this practice is perpetuated and renewed in an art consisting of piecing together various materials into a collage in which family photographs hold a predominant place. As the lines between entertainments, traditional practices and culture blur, it is necessary to question how ethnology approaches these recent and increasingly popular leisure activities. This essay documents the main facets of the scrapbooking practice as it exists in Quebec (Canada). It examines how various aspects of today’s leisure activities influence the creation and transmission of familial heritage. How are today’s personal albums involved in the process of familial heritage creation? This study is based on an ethnological research conducted in the Quebec City region. The oral investigation conducted with scrapbooking lovers made possible the acquirement of knowledge regarding this production and the study of their views on the subject. More specifically, the study is focused on the following aspects: the activity’s logistics and how it relates to creativity and identity, the resulting scrapbooking, the performance context and its influence on the scrapbook’s creation process. Finally, we outlined the role scrapbooking plays in the familial heritage of scrapbookers. As an amateur practice, today’s scrapbooking activity is outside of traditional artistic endeavours due to its renewed form of expression. It is at the heart of several issues related, amongst other things, to mass consumption products and the new information technologies.

Cette recherche vise à établir les propriétés fondamentales d'un système formel aux preuves circulaires introduit par Santocanale, auquel on a rajouté la règle de coupure. On démontre, dans un premier temps, qu'il y a une pleine correspondance entre les preuves circulaires et les flèches issues des catégories dites µ-bicomplètes. Ces flèches sont celles que l'on peut définir purement à partir des outils suivants: les produits et coproduits finis, les algèbres initiales et les coalgèbres finales. Dans la catégorie des ensembles, les preuves circulaires dénotent donc les fonctions qu'on peut définir en utilisant les produits cartésiens finis, les unions disjointes finies, l'induction et la coinduction. On décrit également une procédure d'élimination des coupures qui produit, à partir d'une preuve circulaire finie, une preuve sans cycles et sans coupures, mais possiblement infinie. On démontre que l'élimination des coupures fournit une sémantique opérationnelle aux preuves circulaires, c'est-à-dire qu'elle permet de calculer les fonctions dénotées par celles-ci, par le moyen d'une sorte d'automate avec mémoire. Enfin, on s'intéresse au problème de la puissance expressive de cet éliminateur de coupures, c'est-à-dire à la question de caractériser la classe des expressions qu'il peut calculer. On démontre, par une simulation, que l'éliminateur des coupures est strictement plus expressif que les automates à pile d'ordre supérieur. / This research aims at establishing the fundamental properties of a formal system with circular proofs introduced by Santocanale, to which we added the cut rule. We first show that there is a full correspondence between circular proofs and arrows from the so-called µ-bicomplete categories. These arrows are those that can be defined purely from the following tools: finite products and coproducts, initial algebras and final coalgebras. In the category of sets, circular proofs denote functions that one can define by using finite cartesian products, finite disjoint unions, induction and coinduction. We also describe a cut-elimination procedure that produces, from a given finite circular proof, a proof without cycles and cuts, but which may be infinite. We prove that cut-elimination gives an operational semantics to circular proofs, which is to say that they allow to compute the functions denoted by them, by using a sort of automaton with memory. Finally, we are interested in finding the expressive power of that cut-eliminating automaton. In other words, we want to characterize the class of functions that it can compute. We show, through a simulation, that the cut-eliminating automaton is strictly more expressive than higher-order pushdown automata.

Au-delà de la capacité des systèmes à faire face aux crises sanitaires, investir en prévention devrait se lire « investir pour la santé » dans la perspective plus large d’une amélioration du bien-être des populations. Plusieurs études démontrent que les programmes de santé publique contribuent à prévenir la mortalité, améliorent la qualité de vie et réduisent les coûts des soins de santé sur le court et long terme (Dyakova et al. 2017 ; Masters et al. 2017). Pourtant, le portrait des dépenses de santé dans la plupart des pays suggère un sous-financement inquiétant des dépenses préventives en santé. Ce mémoire propose un cadre formel pour démystifier les dynamiques politiques et financières sous-jacentes à la prise de décision des gouvernements en place en matière d’investissement en santé préventive. Plus précisément, il est question d’analyser les variations des dépenses en santé publique dans les provinces canadiennes de 1975 à 2018. En s’intéressant à l’organisation du système de santé dans son ensemble et au gré des réformes politiques et structurelles des provinces, les résultats de l’analyse qualitative montrent que l’émergence du nouveau management public (NMP) dans les années 1990 a globalement contribué à la diminution accordée à la prévention. L’analyse quantitative quant à elle, énonce les éléments conjoncturels et structurels financiers qui participent à la variation des dépenses en santé publique. En considérant le financement en santé publique comme un investissement à long terme, il a été démontré que les dépenses préventives ne sont pas aussi largement soutenues et constituent des investissements à long terme discrets avec peu d’appuis dans la société. Cela implique, du point de vue financier, que ce type de dépenses est plus propice aux coupures budgétaires, surtout en période de récession et de crise économique. / Beyond the capacity of systems to deal with health crises, investing in prevention should read “investing for health” in the broader perspective of improving the well-being of populations. Several studies demonstrate that public health programs help prevent mortality, improve quality of life and reduce health care costs in the short and long term (Dyakova et al. 2017; Masters et al. 2017). However, the portrait of health expenditure in most countries suggests a worrying underfunding of preventive health expenditure. This thesis proposes a formal framework to demystify the political and financial dynamics underlying the decision-making of governments in place in terms of investment in public health. More specifically, we analyze the variations in public health expenditure in the Canadian provinces from 1975 to 2018. By focusing on the organization of the health system as a whole, according to political and structural reforms over time, the results of the qualitative analysis show that the emergence of new public management (NPM) in the early 1990 contributed overall to the reduction granted to prevention. The quantitative analysis, for its part, sets out the economic and structural financial elements that contribute to the variation in public health expenditure. Viewing public health funding as a long-term investment, it has been shown that preventive spending is not as widely supported and is a discrete long-term investment with little support in society. This implies, from a financial point of view, that this type of spending is more prone to budget cuts, especially in times of recession and economic crisis.