Nous étudions les logiques du temps arborescent en tant qu'outils de spécification et de preuve des programmes. Les différentes logiques modales et temporelles sont comparées par rapport aux deux critères suivantes: puissance d'expression et décidabilité. Cette étude porte essentiellement sur fa comparaison des logiques du temps arborescent et des logiques du temps linéaire. Ensuite, le problème de l'utilisation des logiques du temps arborescent en tant qu'outils de preuves des programmes est étudié. Nous proposons une logique pour la preuve constructive des propriétés des processus contrôlables de CCS. Cette logique est telle, que la relation de congruence induite est la congruence observationnelle de CCS

Nous présentons d'abord les théorèmes du No Free Lunch en nous basant sur le papier de D.H. Wolpert et W.G. Macready (version IEEE 1997) mais aussi les multiples réactions que ces résultats ont provoquées dans la communauté de l'optimisation. Convaincus dès lors de l'intérêt d'une approche globale des problèmes et de la nécessité de la recherche de propriétés générales - et spécialement des invariances par symétries -, nous tentons ensuite de mettre en oeuvre cette méthode dans le cadre de la coloration de graphes simples et non orientés. Ce champ est retenu en raison de son intérêt propre, mais aussi pour son caractère de modèle fécond dans de multiples problèmes d'optimisation. Nous faisons émerger la notion de décomposition d'un graphe en cliques maximales et celle de suites constructives qui permettent de reconstruire un graphe à partir de ses composants élémentaires (primary cliques), véritables équivalents des nombres premiers pour les entiers naturels. Nous produisons un algorithme principal et en étudions deux cas singuliers; ensemble ils fournissent une partition de l'ensemble des colorations valides du graphe étudié. Par suite nous retrouvons le polynôme chromatique de manière formelle, indépendamment du nombre de couleurs disponibles. Nous établissons une correspondance de Galois entre colorations valides et sous-graphes engendrés par des familles emboîtées de cliques maximales pourvu qu'elles soient des décompositions complètes de sous-graphes croissants du graphe total.

Les éco-matériaux présentent un certain nombre de caractéristiques intéressantes comparativement à des solutions techniques ou architecturales classiques. Les critères de différenciation utilisés étaient jusqu'alors souvent liés à la préservation de l'environnement et de la santé. L'objectif de cette thèse est d'étudier les caractéristiques techniques, économiques et financières présentées par ces matériaux plus respectueux de l'environnement en regroupant des informations de référence sélectionnées au sein d'un référentiel proposé. La première partie de ce travail situe la thématique des éco-matériaux dans le contexte de la conception de bâtiments à qualité environnementale. Une deuxième partie précise la place des éco-matériaux au sein des systèmes de management de la qualité environnementale du bâti (SMQEB) internationaux et Européens. Le cahier des charges d'une méthode d'aide au choix d'éco-matériaux y est exposé. La troisième partie concerne la conception d'un outil d'aide à la prescription technique, économique et financière d'éco-matériaux. La dernière partie recentre sur un territoire d'étude la méthodologie élaborée et testée : la région Nord Pas de Calais. Un système constructif élaboré, un rampant de toiture, est utilisé comme base pour la comparaison d'un assemblage de solutions éco-construites et conventionnelles. Les critères techniques, économiques, financiers, environnementaux et de santé utilisés sont in fine traduits en ratio coûts / bénéfices

Au croisement de la sociologie urbaine, de la sociologie de la famille et de l'analyse architecturale, cette thèse traite des transformations qu'apportent les habitants à leur espace domestique, au cours de la seconde moitié du XXe siècle à Tozeur (Jérid, Tunisie). Basée sur une cinquantaine de monographies de maisons, combinant relevés architecturaux et entretiens semi-directifs, l'analyse menée selon une démarche issue de la méthode indiciaire est centrée sur l'évolution de l'habitation et son articulation avec celle de la maisonnée. L'interprétation circonstanciée des traces et des indices révèle les étapes successives de l'occupation domestique. L'évolution du sens des différents termes relevés (ḥûš, dâr...) renseignent sur la définition des espaces et sur l'emprise de la maison. S'ils sont concomitants à l'avènement de nouveaux espaces, les changements technologiques attestent d'une évolution de la notion de confort, de l'apparition de nouveaux acteurs et de transferts de savoir-faire. Les négociations relevées lors des sédentarisations et des rénovations mettent au jour l'influence des procédures réglementaires et des stratégies de contournement différenciées. L'emploi préférentiel de certains matériaux de construction, de modénatures esthétiques et de nouvelles typologies architecturales indique une recherche de positionnement social et sa légitimité. L'enquête renseigne qu'aménager la maison et ordonner la famille sont deux actions simultanées, tout en faisant chacune appel à des discours et des représentations différents. L'examen des dynamiques de transformation de l'habitation, une manifestation d'individus en famille, livre une analyse du corps social.

Cette thèse présente une formalisation des nombres algébriques et de leur théorie. Elle apporte deux nouvelles contributions importantes à la formalisation de résultats mathématiques dans des assistants à la preuve, ici Coq : la construction intuitionniste des nombres algébriques réels et la preuve qu'ils constituent un corps réel clos, ainsi que la programmation et la certification de procédures d'élimination des quantificateurs pour les théories des corps algébriquement clos et des corps réels clos. Pour atteindre ces résultats, nous avons apporté des contributions aux outils et aux méthodologies de preuves et de formalisation des mathématiques en Coq. En particulier, nous fournissons pour Coq/SSReflect un cadre pour travailler avec des types quotients. Nous fournissons une bibliothèque complète sur les structures algébriques de nombres ordonnés et normés. Nous avons réalisé une courte implémentation des réels de Cauchy accompagnée de tactiques pour effectuer facilement des raisonnements comportant des affirmations de la forme "soit n un entier suffisamment grand", couramment utilisés dans les preuves mathématiques sur papier. Nous avons également développé une petite bibliothèque d'analyse de base sur les polynômes à coefficients dans un corps réel clos. Une grande partie de nos résultats s'intègrent dans la formalisation de la preuve du théorème de Feit-Thompson et ont aussi pour objectif d'aider à certifier des procédures plus efficace d'élimination des quantificateurs sur les réels.

Les recherches de cette thèse portent sur la mise en oeuvre des méthodes de la rechercheopérationnelle (RO) pour la conception de circuits numériques dans le domaine du traitementdu signal et de l’image, plus spécifiquement pour des applications multimédia et de visionembarquée.Face à la problématique de “Memory Wall”, les concepteurs de systèmes de vision embarquée,Mancini et al. (Proc.DATE, 2012), ont proposé un générateur de hiérarchies mémoiresad-hoc dénommé Memory Management Optimization (MMOpt). Cet atelier de conception estdestiné aux traitements non-linéaires afin d’optimiser la gestion des accès mémoires de cestraitements. Dans le cadre de l’outil MMOpt, nous abordons la problématique d’optimisationliée au fonctionnement efficace des circuits de traitement d’image générés par MMOpt visantl’amélioration des enjeux de performance (contrainte temps-réel), de consommation d’énergieet de coût de production (contrainte d’encombrement).Ce problème électronique a été modélisé comme un problème d’ordonnancement multiobjectif,appelé 3-objective Process Scheduling and Data Prefetching Problem (3-PSDPP), reflétantles 3 principaux enjeux électroniques considérés. À notre connaissance, ce problème n’apas été étudié avant dans la littérature de RO. Une revue de l’état de l’art sur les principaux travauxliés à cette thèse, y compris les travaux antérieurs proposés par Mancini et al. (Proc.DATE,2012) ainsi qu’un bref aperçu sur des problèmes voisins trouvés dans la littérature de RO,a ensuite été faite. En outre, la complexité de certaines variantes mono-objectif du problèmed’origine 3-PSDPP a été établie. Des approches de résolution, y compris les méthodes exactes(PLNE) et les heuristiques constructives, sont alors proposées. Enfin, la performance de cesméthodes a été comparée par rapport à l’algorithme actuellement utilisé dans l’outil MMOpt,sur des benchmarks disponibles dans la littérature ainsi que ceux fournis par Mancini et al.(Proc.DATE, 2012).Les solutions obtenues sont de très bonne qualité et présentent une piste prometteuse pouroptimiser les performances des hiérarchies mémoires produites par MMOpt. En revanche, vuque les besoins de l’utilisateur de l’outil sont contradictoires, il est impossible de parler d’unesolution unique en optimisant simultanément les trois critères considérés. Un ensemble debonnes solutions de compromis entre ces trois critères a été fourni. L’utilisateur de l’outilMMOpt peut alors décider de la solution qui lui est la mieux adaptée. / The research of this thesis focuses on the application of the Operations Research (OR)methodology to design new optimization algorithms to enable low cost and efficient embeddedvision systems, or more generally devices for multimedia applications such as signal and imageprocessing.The design of embedded vision systems faces the “Memory Wall” challenge regarding thehigh latency of memories holding big image data. For the case of non-linear image accesses, onesolution has been proposed by Mancini et al. (Proc. DATE 2012) in the form of a software tool,called Memory Management Optimization (MMOpt), that creates an ad-hoc memory hierarchiesfor such a treatment. It creates a circuit called a Tile Processing Unit (TPU) that containsthe circuit for the treatment. In this context, we address the optimization challenge set by theefficient operation of the circuits produced by MMOpt to enhance the 3 main electronic designcharacteristics. They correspond to the energy consumption, performance and size/productioncost of the circuit.This electronic problem is formalized as a 3-objective scheduling problem, which is called3-objective Process Scheduling and Data Prefetching Problem (3-PSDPP), reflecting the 3 mainelectronic design characteristics under consideration. To the best of our knowledge, this problemhas not been studied before in the OR literature. A review of the state of the art, including theprevious work proposed by Mancini et al. (Proc.DATE, 2012) as well as a brief overview onrelated problems found in the OR literature, is then made. In addition, the complexity of someof the mono-objective sub-problems of 3-PSDPP problem is established. Several resolutionapproaches, including exact methods (ILP) and polynomial constructive heuristics, are thenproposed. Finally, the performance of these methods is compared, on benchmarks available inthe literature, as well as those provided by Mancini et al. (Proc.DATE, 2012), against the onecurrently in use in the MMOpt tool.The results show that our algorithms perform well in terms of computational efficiency andsolution quality. They present a promising track to optimize the performance of the TPUs producedby MMOpt. However, since the user’s needs of the MMOpt tool are contradictory, such aslow cost, low energy and high performance, it is difficult to find a unique and optimal solutionto optimize simultaneously the three criteria under consideration. A set of good compromisesolutions between these three criteria was provided. The MMOpt’s user can then choose thebest compromise solution he wants or needs.

Dans les régions exposées à des aléas naturels, une large partie des bâtiments composant l'environnement construit sont réalisés presque exclusivement sur la base de l'expérience et de l'observation des bâtisseurs locaux, sans l'appui d'un architecte ou d'un ingénieur. Les communautés installées dans ces zones ont développé, au fil du temps, une multitude de stratégies pour co-habiter avec ces phénomènes, incluant des comportements sociaux et des approches de construction visant à prévenir et/ou à limiter l'exposition du bâti et de ses habitants. En fait, les constructeurs ont souvent intégré la présence et les caractéristiques locales des aléas naturels dans leurs pratiques quotidiennes, élaborant des détails et des dispositions constructives particulières pour réduire la vulnérabilité des artefacts et du milieu bâti. Le concept de culture constructive embrasse la dimension sociale et technique de l'acte de construire et du processus d'élaboration des savoirs et savoir-faire qui lui sont inhérents, reflétant intrinsèquement la multiplicité des sociétés humaines et leur enracinement indissoluble au territoire qu'elles habitent. Le vernaculaire en tant que caractérisation des modes de bâtir, d'habiter et de se protéger se révèle par ce fait une source précieuse de pratiques, techniques et mesures, testées au cours des siècles et des multiples aléas, pour la construction d'environnements bâtis durables, accessibles et sûrs. Ce travail de recherche explore le potentiel présenté par les cultures constructives vernaculaires dans le renforcement de la résilience locale. Et cela à partir des pratiques - constructives et comportementales - développées par les populations, groupes et individus habitant des contextes géographiquement exposés à des aléas naturels. Se fondant sur une forte interaction entre la théorie et la pratique, cette recherche entame une (re)découverte de l'ingéniosité intrinsèque à ces savoirs par le développement de deux axes thématiques. L'un investigue les dispositions et les dispositifs vernaculaires à caractère parasinistre ayant démontré leur efficacité à réduire la vulnérabilité de l'environnement construit envers différents types d'aléas naturels. L'autre axe questionne les modalités de leur identification et contribution directe au renforcement des capacités de populations et institutions dans la gestion des crises. À une analyse technique s'associe l'élaboration d'un outil méthodologique soutenant la mise en place d'une démarche de projet s'ancrant fortement aux spécificités contextuelles selon une logique de continuité, tant culturelle que de pratique, entre passé et futur, entre préparation et réponse aux catastrophes. / In areas prone to natural hazards, many of the buildings that make up the built environment are constructed almost exclusively through the experience and the direct observation of local builders, without the support of any architect or engineer. In these regions, communities have developed over time a variety of strategies to cope with natural phenomena through patterns of social behaviours and building approaches intended to prevent and/or to reduce their exposure to local risks. Similarly, local builders have often integrated natural hazards into their daily practices, developing singular techniques, building details or devices aiming to reduce the vulnerability of the built environment. The concept of building culture embraces the social and technical aspects related to the construction process and to the development of corresponding knowledge and know-how, intrinsically reflecting the multiplicity of human societies and their indissoluble connection with the territories they inhabit. The vernacular as characterization of ways of building, living and protecting oneself proves to be a valuable source of practices, techniques and measures, tested over the years and during multiple hazards, for contemporary construction of sustainable, accessible and safe built-environments. This research explores the potential of vernacular building cultures in enhancing local resilience; and this starting from - constructive and behavioural – practices developed by individual people and groups living in contexts geographically exposed to natural hazards. Based on a strong interaction between theory and action, this research undertakes a (re)discovery of vernacular knowledge through two thematic focuses. One examines disaster resilient vernacular provisions and devices which have demonstrated their effectiveness to reduce vulnerability of the built environment to various types of natural hazards. The other one considers ways for their identification and direct contribution to strengthening capacities of communities and institutions for disaster risk management. This research combines a technical analysis with the development of a methodological tool, contributing to set up a project approach strongly rooted into contextual specificities, linking culture and practice, past experience and future needs, disaster response and preparedness.

L’objectif de cette thèse est de démontrer que π4(S3) ≃ Z/2Z en théorie des types homotopiques. En particulier, c’est une démonstration constructive et purement homotopique. On commence par rappeler les concepts de base de la théorie des types homotopiques et on démontre quelques résultats bien connus sur les groupes d’homotopie des sphères : le calcul des groupes d’homotopie du cercle, le fait que ceux de la forme πk(Sn) avec k < n sont triviaux et la construction de la fibration de Hopf. On passe ensuite à des outils plus avancés. En particulier, on définit la construction de James, ce qui nous permetde démontrer le théorème de suspension de Freudenthal et le fait qu’il existe un entier naturel n tel que π4(S3) ≃ Z/2Z. On étudie ensuite le produit smash des sphères, on construit l’anneau de cohomologie des espaces et on introduit l’invariant de Hopf, ce qui nous permet de montrer que n est égal soit à 1, soit à 2. L’invariant de Hopf nous permet également de montrer que tous les groupes de la forme π4n−1(S2n) sont infinis. Finalement, on construit la suite exacte de Gysin, ce qui nous permet de calculer la cohomologie de CP2 et de démontrer que π4(S3) ≃ Z/2Z, et que plus généralement on a πn+1(Sn) ≃ Z/2Z pour tout n ≥ 3 / The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3

Les éco-matériaux présentent un certain nombre de caractéristiques intéressantes comparativement à des solutions techniques ou architecturales classiques. Les critères de différenciation utilisés étaient jusqu’alors souvent liés à la préservation de l’environnement et de la santé. L’objectif de cette thèse est d’étudier les caractéristiques techniques, économiques et financières présentées par ces matériaux plus respectueux de l’environnement en regroupant des informations de référence sélectionnées au sein d’un référentiel proposé. La première partie de ce travail situe la thématique des éco-matériaux dans le contexte de la conception de bâtiments à qualité environnementale. Une deuxième partie précise la place des éco-matériaux au sein des systèmes de management de la qualité environnementale du bâti (SMQEB) internationaux et Européens. Le cahier des charges d’une méthode d’aide au choix d’éco-matériaux y est exposé. La troisième partie concerne la conception d’un outil d’aide à la prescription technique, économique et financière d’éco-matériaux. La dernière partie recentre sur un territoire d’étude la méthodologie élaborée et testée : la région Nord Pas de Calais. Un système constructif élaboré, un rampant de toiture, est utilisé comme base pour la comparaison d’un assemblage de solutions éco-construites et conventionnelles. Les critères techniques, économiques, financiers, environnementaux et de santé utilisés sont in fine traduits en ratio coûts / bénéfices / Eco-materials, have revealed a number of interesting characteristics compared with more traditional technical or architectural solutions. The criteria so far used to differentiate them were often related to the preservation of the environment or health. The main research objective has been to study the technical, economic and financial advantages of such more environmentally friendly materials by collecting selected referential information- assessment indicators and criteria- inside a proposed system of reference. The first part of my work has been devoted to identifying eco-materials in the broader context of the conception of high environmental quality buildings. The position of eco-materials in international and European Environmental Quality Management Systems for Buildings- SMQEB- has then been reviewed in a second part. The third part of this work has consisted in designing a technical, economic and financial prescription decision tool for eco –materials. In the final part, the main concern has been to implement this designed and tested methodology within the Nord Pas De Calais region. An elaborate construction system - a flat roof - has been selected to compare a set of eco-built solutions with more conventional ones. The technical, economic, financial, environmental and health criteria have in-fine been used in easily understood language: the cost/profit ratio