L'objectif de ce travail est d'étudier les détails des écoulements et des transferts thermiques induits par convection naturelle au sein d'un canal (simulation bidimensionnelle) et au sein d'une cavité cubique (simulation tridimensionnelle) munis de blocs chauffants. La chaleur dégagée par les blocs résulte d'une génération volumique uniforme de la chaleur, d'une température chaude constante ou d'un flux surfacique uniforme. On utilise l'air (Pr=0.72) comme fluide. Les paramètres de l'étude sont le rapport des conductivités thermiques du bloc solide et du fluide (0.1≤k*≤200), le nombre de Rayleigh (〖10〗^4≤Ra≤〖10〗^7) et la hauteur relative des blocs (1/8≤B≤1/2). La détermination des conditions de validité du modèle à blocs isothermes et du modèle à blocs libérant un flux surfacique uniforme, en fonction du rapport des conductivités thermiques et des autres paramètres du problème, compte parmi les principaux objectifs de ce travail. Les résultats obtenus montrent que l'écoulement et le transfert thermique ainsi que les conditions de validité des modèles mentionnés sont fortement influencés par les paramètres de contrôle et par la multiplicité de solutions trouvée en régime convectif. / The object of this work is to study the details of the flow and heat transfer induced by natural convection in a channel (2D simulation) and in a cubic cavity (3D simulation) containing heating blocks. The heat released by the blocks results from a uniform volumetric heat generation, a constant hot temperature or a uniform surface flux. Air (Pr=0.72) is used as working fluid. The parameters of the study are the thermal conductivities ratio of solid blocks and fluid (0.1≤k*≤200), the Rayleigh number (〖10〗^4≤Ra≤〖10〗^7) and the relative height of the blocks (1/8≤B≤1/2). Among the main objects of this work is the determination of the conditions of validity of the model with isothermal blocks and the model with blocks releasing a uniform surface flux, as functions of the thermal conductivities ratio and the other parameters of the problem. The results obtained show that the flow and heat transfer and the conditions of validity of the models mentioned are strongly affected by the control parameters and the multiplicity of solutions found in the convective regime.

Cette thèse s'intéresse à la métathéorie de la théorie des types intuitionniste. Les systèmes que nous considérons sont des variantes de la théorie des types de Martin-Löf ou du Calcul des Constructions, et nous nous intéressons à la cohérence de ces systèmes ou encore à l'indépendance d'axiomes par rapport à ces systèmes. Le fil rouge de cette thèse est la construction de modèles syntaxiques, qui sont des modèles qui réutilisent la théorie des types pour interpréter la théorie des types. Dans une première partie, nous introduisons la théorie des types à l'aide d'un système minimal et de plusieurs extensions potentielles. Dans une seconde partie, nous introduisons les modèles syntaxiques donnés par traduction de programme et donnons plusieurs exemples. Dans une troisième partie, nous présentons Template-Coq, un plugin de métaprogrammation pour Coq. Nous montrons comment l'utiliser pour implémenter directement certains modèles syntaxiques. Enfin, dans une dernière partie, nous nous intéressons aux théories des types à deux égalités : une égalité stricte et une égalité univalente. Nous proposons une relecture des travaux de Coquand et. al. et Orton et Pitts sur le modèle cubique en introduisant la notion de fibrance dégénérée. / This thesis is about the metatheory of intuitionnistic type theory. The considered systems are variants of Martin-Löf type theory of Calculus of Constructions, and we are interested in the coherence of those systems and in the independence of axioms with respect to those systems. The common theme of this thesis is the construction of syntactic models, which are models reusing type theory to interpret type theory. In a first part, we introduce type theory by a minimal system and several possible extensions. In a second part, we introduce the syntactic models given by program translation and give several examples. In a third part, we present Template-Coq, a plugin for metaprogramming in Coq. We demonstrate how to use it to implement directly some syntactic models. Last, we consider type theories with two equalities: one strict and one univalent. We propose a re-reading of works of Coquand et.al. and of Orton and Pitts on the cubical model by introducing degenerate fibrancy.