Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit pas pour vérifier des critères plus complexes comme l'absence de divisions par zéro. Cette thèse est consacrée à l’étude d’une extension de la logique d’ordre supérieur appelée sous-typage par prédicats (predicate subtyping), dont l'objet est de rendre l'attribution de types aussi expressive que l'attribution de prédicats. A partir d'un type A et d'un prédicat P(x) de domaine A, le sous-typage par prédicats permet de construire un sous-type de A, noté {x : A | P(x)}, dont les éléments sont les termes t de type A tels que P(t) est démontrable. Le sous-typage par prédicats est au coeur du système PVS.Ce travail présente la formalisation d'un système minimal incluant le sous-typage par prédicats, appelé PVS-Core, ainsi qu'un système de certificats vérifiables pour PVS-Core. Ce deuxième système, appelé PVS-Cert, repose sur l'introduction de termes de preuves et de coercions explicites. PVS-Core et PVS-Cert sont munis d'une notion de conversion correspondant respectivement à l'égalité modulo beta et à l'égalité modulo beta et effacement des coercions, choisi pour établir une correspondance simple entre les deux systèmes.La construction de PVS-Cert est semblable à celle des PTS (Pure Type Systems) avec paires dépendantes et PVS-Cert peut être muni de la notion de beta-sigma-réduction utilisée au coeur de ces systèmes. L'un des principaux théorèmes démontré dans ce travail est la normalisation forte de la réduction sous-jacente à la conversion et de la beta-sigma-réduction. Ce théorème permet d'une part de construire un algorithme de vérification du typage (et des preuves) pour PVS-Cert et d'autre part de démontrer un résultat d'élimination des coupures, utilisé à son tour pour prouver plusieurs propriétés importantes des deux systèmes étudiés. Par ailleurs, il est également démontré que PVS-Cert est une extension conservative du PTS lambda-HOL, et qu'en conséquence PVS-Core est une extension conservative de la logique d'ordre supérieur.Une deuxième partie présente le prototype d'une instrumentation de PVS pour produire des certificats de preuve. Une troisième et dernière partie est consacrée à l'étude de liens entre logique classique et constructive avec la définition d'une traduction par double négation minimale ainsi que la présentation d'un algorithme de constructivisation automatique des preuves. / The type system of higher-order logic allows to exclude some unexpected expressions such as the application of a predicate to itself. However, it is not sufficient to verify more complex criteria such as the absence of divisions by zero. This thesis is dedicated to the study of an extension of higher-order logic, named predicate subtyping, whose purpose is to make the assignment of types as expressive as the assignment of predicates. Starting from a type A and a predicate P(x) of domain A, predicate subtyping allows to build a subtype of A, denoted {x : A | P(x)}, whose elements are the terms t of type A such that P(t) is provable. Predicate subtyping is at the heart of the proof system PVS.This work presents the formalization of a minimal system expressing predicate subtyping, named PVS-Core, as well as a system of verifiable certificates for PVS-Core. This second system, named PVS-Cert, is based on the introduction of proof terms and explicit coercions. PVS-Core and PVS-Cert are equipped with a notion of conversion corresponding respectively to equality modulo beta and to equality modulo beta and the erasure of coercions, chosen to establish a simple correspondence between the two systems.The construction of PVS-Cert is similar to that of PTSs (Pure Type Systems) with dependent pairs and PVS-Cert can be equipped with the notion of beta-sigma-reduction used at the core of these systems. One of the main theorems proved in this work is the strong normalization of both the reduction underlying the conversion and beta-sigma-reduction. This theorem allows, on the one hand, to build a type-checking (and proof-checking) algorithm for PVS-Cert and, on the other hand, to prove a cut elimination result, used in turn to prove important properties of the two studied systems. Furthermore, it is also proved that PVS-Cert is a conservative extension of the PTS lambda-HOL and that, as a consequence, PVS-Core is a conservative extension of higher-order logic.A second part presents the prototype of an instrumentation of PVS to generate proof certificates. A third and final part is dedicated to the study of links between classical and constructive logic, with the definition of a minimal double-negation translation as well as the presentation of an automated proof constructivization algorithm.

L'objectif de ce mémoire est dedévelopper de nouvelles méthodes d'imageriesans lentille en simple tir 2D et 3D avec dessources harmoniques XUV. Un intérêt particulierest porté aux techniques d'imageries permettantl'imagerie des objets biologiques et de phase.Dans un premier temps, on introduit la théorie del'imagerie dans lentille et on détaille lesméthodes utilisées au cours de cette thèse pourreconstruire le champ diffracté par l'objet quel'on souhaite imager. Les techniques d'imageriessont séparées en deux catégories : itératifs etholographiques. On discute des conditionsexpérimentales nécessaires à la reconstruction del'image de l'objet et on compare les avantagesrespectifs des deux types de méthodes. Puis, ondétaille les aspects expérimentaux du faisceauXUV obtenu par HHG et on couvre brièvementla théorie associée à ce processus. La sectionsuivante traite des paramètres et des techniquesde traitement des données influant sur la qualitéde l'image reconstruite en imagerie sans lentille.On montre comment améliorer lesreconstructions HERALDO dans un régime defaible flux de photons. On présente ensuite lesrésultats d'une technique de caractérisationcomplète de la cohérence spatiale d’un faisceauXUV en simple tir. Cette dernière est unparamètre critique de l'imagerie sans lentille. Al'aide d'un tableau non redondant de référencesponctuelles, on mesure la cohérence spatialepour chaque distance entre les références, sansaucune mesure du profil spatial du faisceau. Onmontre que la distribution de la cohérence estgaussienne et que son diamètre dépend desconditions de génération du faisceauharmonique. On étudie aussi quantitativementcomment l'accumulation de plusieurs tirs dediffraction diminue la cohérence apparente dufaisceau. Une expérience d'imagerie d'objets dephase avec une source harmonique pouvant êtreappliquée à des objets biologiques est ensuiteprésentée.A notre connaissance c'est la premièrereconstruction par méthode CDI d'objets dephase avec une source harmonique. La suite dumanuscrit présente les résultats de deuxexpériences visant à réaliser de l'imagerie 3D àl'échelle nanométrique avec une sourceharmonique. Tout d’abord, on présente unetechnique d'imagerie 3D simple tir. C'est lapremière expérience permettant unereconstruction 3D à partir d'une seuleacquisition, avec une résolution spatialenanométrique et une résolution temporellefemtoseconde, sans utiliser de connaissances apriori sur l'objet étudié. Cette technique possèdeun vaste spectre d'application, particulièrementpour l'étude structurelle d'échantillonsbiologiques sensibles aux dégâts d'irradiation.De plus, cette technique peut être facilementapplicable à des FELs et des synchrontrons pourobtenir de meilleures résolutions. La deuxièmeexpérience d'imagerie 3D est une preuve deconcept validant la faisabilité de lacryptomographie avec une source harmonique.Pour reconstruire le volume 3D de l'échantillon,la cryptotomographie utilise des figures dediffraction qui sont acquises pour desorientations de l'échantillon inconnues. Lerégime de faible flux dans lequel on se place nouspermet de simuler les paramètres d'une sourceharmonique fonctionnant dans la fenêtre de l'eau.On conclut que, le niveau du signal de diffractionest suffisant pour pouvoir identifier l'orientationde l'objet à partir des figures de diffractionenregistrées, dans des conditions expérimentalesoptimisées. Ainsi, avec suffisamment de figuresde diffraction enregistrées et assez d'orientationsde l'objet, on peut reconstruire le volume 3D del'objet. Ces résultats impliquent qu'uneexpérience de cryptotomographie d'objetsbiologiques avec une source harmoniquefonctionnant dans la fenêtre de l'eau seraitréalisable. / The aim of this dissertation is todevelop new lensless single shot imagingtechnique in 2D and 3D with XUV harmonicsources which can be applied to study biologicalobjects and phase objects. Firstly, we introducethe theory underlying lensless imagingtechniques and we describe the methods usedduring this thesis to reconstruct the light fielddiffracted by the studied object. The imagingtechniques are split in two categories: iterativeand holographic. The iterative methodsreconstruct the phase of the diffracted wavefront using constraints in the Fourier space andthe reel space. With the holographic techniques,the phase is encoded directly in the interferencefringes between the reference and the objectwithin the diffraction pattern. We discuss theexperimental parameters required to achieve animage reconstruction and we compare therespective advantages of the two types ofmethod. Then, we describe the experimentalparameters of the XUV beam produced by highharmonic generation (HHG) and we brieflyexplain the theory of the HHG. The next sectiondiscusses the parameters the quality of thereconstructed image. We show how to improvethe resolution and the signal to noise ratio usingthe HERALDO technique in the low fluxregime.We then show the result of a new technique forthe single shot characterization of the spatialcoherence of XUV beams. Indeed, the spatialcoherence is a critical parameter for coherentdiffractive imaging techniques. Using a NRA ofreference holes, we measure the spatialcoherence for each distance between each pairof holes, without the knowledge of the intensitydistribution on the sample. We show that thespatial coherence has a gaussian distribution andthat its diameter varies according to thegeneration parameters of the harmonic beam.We also study quantitatively the effect of multishotsaccumulation of the diffraction pattern onthe apparent coherence of the beam. We alsoshow the result of phase object imaging usingcoherent diffractive imaging with a harmonicsource. To our knowledge, this if the first timesuch result has been achieved. The rest of thedissertation present new lensless imaging 3Dtechniques using harmonic sources. The first ofthe last two experiments shown is a lenslesssingle shot stereo 3D technique. It is the first oneallowing a 3D reconstruction from a singleacquisition, with a nanometer spatial resolutionand a femtosecond temporal resolution, withoutusing \textit{a priori} knowledge of the samplestudied. This method has a vast spectrum ofapplication and is particularly interesting for thestructural study of biological sample sensitive toradiation damage and for the study of nonreversibledynamical phenomena in 3D.Furthermore, this can easily be implemented inFELs and synchrotrons to reach even betterspatial resolution. The second 3D experimentshown in this thesis is a proof of concept ofcryptotomography using a high harmonic sourcein a low flux regime. To reconstruct the 3Dvolume of the sample, cryptotomographie usesdiffraction pattern acquired for unknown sampleorientations and therefore non-classified. Thelow flux regime used here simulate the flux of aharmonic source generated in the water window.We conclude from this experiment that, with theproper experimental conditions, the diffractionsignal is sufficient to allow the classification byorientation of the diffraction patterns. Withenough diffraction pattern and angles of thesample recorded, we can achieve a 3Dreconstruction of the sample. This result impliesthat the cryptotomography of biological objectsusing a water window harmonic source ispossible.

Ce manuscrit de thèse est consacré à l'analyse mathématique et numérique des systèmes de l'hydrodynamique compressible et de la photonique. Plus particulièrement, on étudie la construction de méthodes numériques dans des systèmes de coordonnées 2D polaires (une coordonnée radiale et une coordonnée d'angle) et où les équations sont discrétisées sur des maillages polaires structurés. Ces méthodes sont adaptées à la simulation d'écoulements à symétrie polaire puisqu'elles préservent ces symétries par construction. En revanche, ces systèmes de coordonnées introduisent des singularités géométriques et des termes sources géométriques qui doivent être traités avec attention. Dans la première partie de ce document, consacrée à l'hydrodynamique, on propose une classe de schémas numériques d'ordre arbitrairement élevé pour la résolution des équations d'Euler. Ces schémas utilisent des méthodes de résolution à directions alternées où chaque sous-système est résolu par un solveur Lagrange+projection. On étudie l'influence de la singularité géométrique r=0 des systèmes de coordonnées cylindriques et sphériques sur la précision du solveur 2D développé. La deuxième partie de ce manuscrit est consacrée à l'étude des équations de la photonique. Ces équations font intervenir un grand nombre de dimensions mathématiques et un terme source pouvant être raide. La principale difficulté ici est de capturer le bon régime asymptotique sur maillage grossier. On construit d'abord une classe de modèles où l'intensité radiative est projetée sur une base d'harmoniques sphériques afin de réduire le nombre de dimensions. Puis on propose un schéma numérique en coordonnées polaires et on prouve que le schéma restitue la bonne limite de diffusion aussi bien dans la direction radiale que dans la direction angulaire. / This thesis deals with the mathematical and numerical analysis of the systems of compressible hydrodynamics and radiative transfer. More precisely, we study the derivation of numerical methods with 2D polar coordinates (one for the radius, one for the angle) where equations are discretized on regular polar grids. On one hand, these methods are well-suited for the simulation of flows with polar symetries since they preserve these symetries by construction. On the other hand, such coordinates systems introduce geometrical singularities as well as geometrical source terms which must be carefully treated. The first part of this document is devoted to the study of hydrodynamics equations, or Euler equations. We propose a new class of arbitrary high-order numerical schemes in both space and time and rely on directional splitting methods for the resolution of 2D equations. Each sub-system is solved using a Lagrange+Remap solver. We study the influence of the r=0 geometrical singularities of the cylindrical and spherical coordinates systems on the precision of the 2D numerical solutions. The second part of this document is devoted to the study of radiative transfer equations. In these equations, the unknowns depend on a large number of variables and a stiff source term is involved. The main difficulty consists in capturing the correct asymptotic behavior on coarse grids. We first construct a class of models where the radiative intensity is projected on a truncated spherical harmonics basis in order to lower the number of mathematical dimensions. Then we propose an Asymptotic Preserving scheme built in polar coordinates and we show that the scheme capture the correct diffusion limit in the radial direction as well as in the polar direction.

La simulation numérique de phénomènes physiques complexes requiert généralement l’utilisation d’un maillage. En mécanique des fluides numérique, cela consisteà représenter un objet dans un gros volume de contrôle. Cet objet étant celui dont l’on souhaite simuler le comportement. Usuellement, l’objet et la boîte englobante sont représentés par des maillage de surface linéaires et la zone intermédiaire est remplie par un maillage volumique. L’objectif de cette thèse est de s’intéresser à deux manières différentes de représenter cet objet. La première approche dite immergée consiste à mailler intégralement le volume de contrôle et ensuite à simuler le comportement autour de l’objet sans avoir à mailler explicitement dans le volume ladite géometrie. L’objet étant implicitement pris en compte par le schéma numérique. Le couplage de cette méthode avec de l’adaptation de maillage linéaire est notamment étudié. La deuxième approche dite d’ordre élevé consiste quant à elle consiste à augmenter le degré polynomial du maillage de surface de l’objet. La première étape consiste donc à générer le maillage de surface de degré élevé et ensuite àpropager l’information de degré élevé dans les éléments volumiques environnants si nécessaire. Dans ce cadre-là, il s’agit de s’assurer de la validité de telles modifications et à considérer l’extension des méthodes classiques de modification de maillages linéaires. / The numerical simulation of complex physical phenomenons usually requires a mesh. In Computational Fluid Dynamics, it consists in representing an object inside a huge control volume. This object is then the subject of some physical study. In general, this object and its bounding box are represented by linear surface meshes and the intermediary zone is filled by a volume mesh. The aim of this thesis is to have a look on two different approaches for representing the object. The first approach called embedded method consist in integrally meshing the bounding box volume without explicitly meshing the object in it. In this case, the presence of the object is implicitly simulated by the CFD solver. The coupling of this method with linear mesh adaptation is in particular discussed.The second approach called high-order method consist on the contrary by increasing the polynomial order of the surface mesh of the object. The first step is therefore to generate a suitable high-order mesh and then to propagate the high-order information in the neighboring volume if necessary. In this context, it is mandatory to make sure that such modifications are valid and then the extension of classic mesh modification techniques has to be considered.

La simulation aux grandes échelles est devenue un outil d’analyse incontournable pour l’étude des écoulements turbulents dans des géométries complexes. Cependant, à cause de l’augmentation constante des ressources de calcul, le traitement des grandes quantités de données générées par les simulations hautement résolues est devenu un véritable défi qu’il n’est plus possible de relever avec des outils traditionnels. En mécanique des fluides numérique, cette problématique émergente soulève les mêmes questions que celles communément rencontrées en informatique avec des données massives. A ce sujet, certaines méthodes ont déjà été développées telles que le partitionnement et l’ordonnancement des données ou bien encore le traitement en parallèle mais restent insuffisantes pour les simulations numériques modernes. Ainsi, l’objectif de cette thèse est de proposer de nouveaux formalismes permettant de contourner le problème de volume de données en vue des futurs calculs exaflopiques que l’informatique devrait atteindre en 2020. A cette fin, une méthode massivement parallèle de co-traitement, adaptée au formalisme non-structuré, a été développée afin d’extraire les grandes structures des écoulements turbulents. Son principe consiste à introduire une série de grilles de plus en plus grossières réduisant ainsi la quantité de données à traiter tout en gardant intactes les structures cohérentes d’intérêt. Les données sont transférées d’une grille à une autre grâce à l’utilisation de filtres et de méthodes d’interpolation d’ordre élevé. L’efficacité de cette méthodologie a pu être démontrée en appliquant des techniques de décomposition modale lors de la simulation 3D d’une pale de turbine turbulente sur une grille de plusieurs milliards d’éléments. En outre, cette capacité à pouvoir gérer plusieurs niveaux de grilles au sein d’une simulation a été utilisée par la suite pour la mise en place de calculs basés sur une stratégie multi-niveaux. L’objectif de cette méthode est d’évaluer au cours du calcul les erreurs numériques et celles liées à la modélisation en simulant simultanément la même configuration pour deux résolutions différentes. Cette estimation de l’erreur est précieuse car elle permet de générer des grilles optimisées à travers la construction d’une mesure objective de la qualité des grilles. Ainsi, cette méthodologie de multi-résolution tente de limiter le coût de calcul de la simulation en minimisant les erreurs de modélisation en sous-maille, et a été appliquée avec succès à la simulation d’un écoulement turbulent autour d’un cylindre. / Large-Eddy Simulation (LES) has become a major tool for the analysis of highly turbulent flows in complex geometries. However, due to the steadily increase of computational resources, the amount of data generated by well-resolved numerical simulations is such that it has become very challenging to manage them with traditional data processing tools. In Computational Fluid Dynamics (CFD), this emerging problematic leads to the same "Big Data" challenges as in the computer science field. Some techniques have already been developed such as data partitioning and ordering or parallel processing but still remain insufficient for modern numerical simulations. Hence, the objective of this work is to propose new processing formalisms to circumvent the data volume issue for the future 2020 exa-scale computing objectives. To this aim, a massively parallel co-processing method, suited for complex geometries, was developed in order to extract large-scale features in turbulent flows. The principle of the method is to introduce a series of coarser nested grids to reduce the amount of data while keeping the large scales of interest. Data is transferred from one grid level to another using high-order filters and accurate interpolation techniques. This method enabled to apply modal decomposition techniques to a billion-cell LES of a 3D turbulent turbine blade, thus demonstrating its effectiveness. The capability of performing calculations on several embedded grid levels was then used to devise the multi-resolution LES (MR-LES). The aim of the method is to evaluate the modeling and numerical errors during an LES by conducting the same simulation on two different mesh resolutions, simultaneously. This error estimation is highly valuable as it allows to generate optimal grids through the building of an objective grid quality measure. MR-LES intents to limit the computational cost of the simulation while minimizing the sub-grid scale modeling errors. This novel framework was applied successfully to the simulation of a turbulent flow around a 3D cylinder.

La plasmonique étudie le couplage entre le rayonnement électromagnétique et les oscillations collectives des électrons dans un matériel. Les plasmons de surface (SPs), notamment, ont la capacité de concentrer le champ électromagnétique sur des distances micrométriques, ce qui les rend intéressants pour le développement des dispositifs photoniques les plus novateurs. 'Etendre l'excitation de SPs au régime de champs élevés, où les électrons oscillent à des vitesses relativistes, ouvre des perspectives stimulantes pour la manipulation de la lumière laser ultra-intense et le développement de sources de rayonnement énergétiques et à courte durée. En fait, l'excitation de modes résonnants du plasma est l'une des stratégies possibles pour transférer efficacement l'énergie d'une impulsion laser ultra-puissante à une cible solide, cela étant parmi les défis actuels dans la physique de l’interaction laser-matière à haute intensité. Dans le cadre de ces deux sujets, ce travail de thèse démontre la possibilité d'exciter de façon résonnante des plasmons de surface avec des impulsions laser ultra-intenses. Elle étudie comment ces ondes peuvent à la fois accélérer de paquets d'électrons relativistes le long de la surface de la cible mais aussi augmenter la génération d'harmoniques d'ordre élevé de la fréquence laser. Ces deux processus ont été caractérisés avec de nombreuses expériences et simulations numériques. En utilisant un schéma d’interaction standard de la plasmonique classique, les SPs sont excités sur des cibles dont la surface présente une modulation périodique régulière à l'échelle micrométrique (cibles réseau). Dans ce cas, les propriétés de l'émission d'électrons tout comme celles des harmoniques permettent d’envisager leur utilisation dans des application pratiques. En réussissant à dépasser les principaux problèmes conceptuels et techniques qui jusqu'au présent avaient empêché l'application d'effets plasmoniques dans le régime de champs élevés, ces résultats apportent un intérêt nouveau à l'exploration de la Plasmonique Relativiste. / Plasmonics studies how the electromagnetic radiation couples with the collective oscillations of the electrons within a medium. Surface plasmons (SPs), in particular, have a well-established role in the development of forefront photonic devices, as they allow for strong enhancement of the local EM field over sub-micrometric dimensions. Promoting the SP excitation to the high-field regime, where the electrons quiver at relativistic velocities, would open stimulating perspectives for the both the manipulation of ultra-intense laser light and the development of energetic, short radiation sources. Indeed, the excitation of resonant plasma modes is a possible strategy to efficiently deliver the energy of a high-power laser to a solid target, this being among the current challenges in the physics of highly-intense laser-matter interaction. Gathering these topics, this thesis demonstrates the opportunity of resonant surface plasmon excitation at ultra-high laser intensities by studying how such waves accelerate bunches of relativistic electrons along the target surface and how they enhance the generation of high-order harmonics of the laser frequency. Both these processes have been investigated with numerous experiments and extensive numerical simulations. Adopting a standard configuration from classical plasmonics, SPs are excited on solid, wavelength-scale grating targets. In their presence, both electron and harmonic emissions exhibit remarkable features that support the conception of practical applications. Putting aside some major technical and conceptual issues discouraging the applicability of plasmonic effects in the high-field regime, these results are expected to mark new promises to the exploration of Relativistic Plasmonics.

Des sources des rayons XUV (1-100 nm) sont des outils extraordinaires pour sonder la dynamique à l’échelle nanométrique avec une résolution femto- voire attoseconde. La génération d’harmoniques d’ordre élevé (GH) est une des sources majeures dans ce domaine d’application. La GH est un processus dans lequel une impulsion laser infrarouge femtoseconde est convertie, de manière cohérente, en fréquences élevées dans le domaine EUV par interaction hautement non-linéaire dans un atome, une molécule et plus récemment, dans un cristal. La GH possède une excellente cohérence spatiale qui a permis de réaliser des démonstrations impressionnantes en imagerie sans lentille. Pour accroître le potentiel de ces sources, des défis sont à relever : leur brillance et énergie de photon maximum doivent augmenter et les techniques d’imagerie sans lentille doivent être modifiées pour être compatibles avec l’importante largeur spectrale des impulsions attosecondes émise par ces sources. Cette thèse présente une nouvelle approche dans laquelle des figures de diffraction large bande, i.e. potentiellement attosecondes, sont rendues monochromatiques numériquement. Cette méthode est basée uniquement sur la mesure du spectre de la source et la supposition d’un échantillon spatialement non-dispersif. Cette approche a été validée tout d’abord dans le visible, à partir d’un supercontinuum. L’échantillon binaire est reconstruit par recouvrement de phase pour une largeur spectrale de 11 %, là où les algorithmes usuels divergent. Les simulations numériques montrent aussi que la méthode de monochromatisation peut être appliquée au domaine des rayons X, avec comme exemple un masque semi-conducteur utilisé en de lithographie EUV. Bien que la brillance « cohérente » de la source actuelle (qui progresse) reste insuffisante, une application sur l’inspection de masques sur source Compton est proposée. Dans une extension de ces simulations un masque de lithographie étendu est reconstruit par ptychographie, démontrant la versatilité à d’autres techniques d’imagerie sans lentille. Nous avons également entamé une série d’expérience dans le domaine des X-durs sur source synchrotron. Les figures de diffraction après monochromatisation numérique semblent prometteuses mais l’analyse des données demandent des efforts supplémentaires. Une partie importante de cette thèse est dédiée à l’extension des sources harmoniques à des brillances et énergies de photon plus élevées. Ce travail exploratoire permettrait la réalisation d’une source harmonique compacte pompée par un laser OPCPA dans le moyen infrarouge à très fort taux de répétition. Les longueurs d’onde moyen infrarouge (3.1 μm dans ce travail de thèse) sont favorables à l’extension des énergies des photons au keV et aux impulsions attosecondes. Le but est de pouvoir couvrir les seuils d’absorption X et d’améliorer la résolution spatio-temporelle. Cependant, deux facteurs rendent cette démonstration difficile: le nombre de photons par impulsion de la source OPCPA est très limité et la réponse du dipôle harmonique à grande longueur est extrêmement faible. Pour relever ces défis plusieurs configurations expérimentales sont explorées : génération dans un jet de gaz ; génération dans une cellule de gaz ; compression solitonique et la génération d’harmoniques combinées dans une fibre à cristal photonique ; compression solitonique dans une fibre à cristal photonique et génération d’harmoniques dans une cellule de gaz. Les premiers résultats expérimentaux sur la compression solitonique jusqu’à 26 femtosecondes et des harmoniques basses jusqu’à l’ordre sept sont présentésEn résumé, ces résultats représentent une avancée vers l’imagerie nanométrique attoseconde sans lentille basée sur des algorithmes « large bande » innovants et une extension des capacités de nouvelles sources harmoniques ‘table-top’ au keV pompées par laser OPCPA. / Soft X-ray sources based on high harmonic generation are up to now unique tools to probe dynamics in matter on femto- to attosecond timescales. High harmonic generation is a process in which an intense femtosecond laser pulse is frequency upconverted to the UV and soft X-ray region through a highly nonlinear interaction in a gas. Thanks to their excellent spatial coherence, they can be used for lensless imaging, which has already led to impressive results. To use these sources to the fullest of their potential, a number of challenges needs to be met: their brightness and maximum photon energy need to be increased and the lensless imaging techniques need to be modified to cope with the large bandwidth of these sources. For the latter, a novel approach is presented, in which broadband diffraction patterns are rendered monochromatic through a numerical treatment based solely on the spectrum and the assumption of a spatially non-dispersive sample. This approach is validated through a broadband lensless imaging experiment on a supercontinuum source in the visible, in which a binary sample was properly reconstructed through phase retrieval for a source bandwidth of 11 %. Through simulations, the numerical monochromatization method is shown to work for hard X-rays as well, with a simplified semiconductor lithography mask as sample. A potential application of lithography mask inspection on an inverse Compton scattering source is proposed, although the conclusion of the analysis is that the current source lacks brightness for the proposal to be realistic. Simulations with sufficient brightness show that the sample is well reconstructed up to 10 % spectral bandwidth at 8 keV. In an extension of these simulations, an extended lithography mask sample is reconstructed through ptychography, showing that the monochromatization method can be applied in combination with different lensless imaging techniques. Through two synchrotron experiments an experimental validation with hard X-rays was attempted, of which the resulting diffraction patterns after numerical monochromatization look promising. The phase retrieval process and data treatment however require additional efforts.An important part of the thesis is dedicated to the extension of high harmonic sources to higher photon energies and increased brightness. This exploratory work is performed towards the realization of a compact high harmonic source on a high repetition rate mid-IR OPCPA laser system, which sustains higher average power and longer wavelengths compared to ubiquitous Ti:Sapphire laser systems. High repetition rates are desirable for numerous applications involving the study of rare events. The use of mid-IR wavelengths (3.1 μm in this work) promises extension of the generated photon energies to the kilo-electronvolt level, allowing shorter pulses, covering more X-ray absorption edges and improving the attainable spatial resolution for imaging. However, high repetition rates come with low pulse energies, which constrains the generation process. The generation with longer wavelengths is challenging due to the significantly lower dipole response of the gas. To cope with these challenges a number of experimental configurations is explored theoretically and experimentally: free-focusing in a gas-jet; free-focusing in a gas cell; soliton compression and high harmonic generation combined in a photonic crystal fiber; separated soliton compression in a photonic crystal fiber and high harmonic generation in a gas cell. First results on soliton compression down to 26 fs and lower harmonics up to the seventh order are presented.Together, these results represent a step towards ultrafast lensless X-ray imaging on table-top sources and towards an extension of the capabilities of these sources.

Dans la première partie de cette thèse, on présente des bornes supérieures fines pour le nombre de sous-variétés irréductibles de torsion maximales dans une sous-variété du tore complexe algébrique $(\mathbb{C}^{\times})^n$ et d'une variété abélienne. Dans les deux cas, on donne une borne explicite en termes du degré des polynômes définissants et la variété ambiante. De plus, la dépendance en le degré des polynômes est optimale. Dans le cas du tore complexe, on donne aussi une borne explicite en termes du degré torique de la sous-variété. En conséquence de ce dernier résultat, on démontre les conjectures de Ruppert, et Aliev et Smyth pour le nombre de points de torsion isolés dans une hypersurface. Ces conjectures bornent ce nombre en terme, respectivement, du multi-degré et du volume du polytope de Newton d'un polynôme définissant l'hypersurface.Dans la deuxième partie de cette thèse, on présente une borne supérieure pour la hauteur des zéros isolés, dans le tore, d'un système de polynômes de Laurent sur un corps adélique qui satisfait la formule du produit. Cette borne s'exprime en termes des intégrales mixtes des fonctions toit locales associées à la hauteur choisie et le système des polynômes de Laurent. On montre aussi que cette borne est presque optimale dans quelques familles d'exemples. Ce résultat est un analogue arithmétique du théorème de Bern\v{s}tein-Ku\v{s}nirenko. / In the first part of this thesis we present sharp bounds on the number of maximal torsion cosets in a subvariety of a complex algebraic torus $(\mathbb{C}^{\times})^n$ and of an Abelian variety. In both cases, we give an explicit bound in terms of the degree of the defining polynomials and the ambient variety. Moreover, the dependence on the degree of the polynomials is sharp. In the case of the complex torus, we also give an effective bound in terms of the toric degree of the subvariety. As a consequence of the latter result, we prove the conjectures of Ruppert, and Aliev and Smyth on the number of isolated torsion points of a hypersurface. These conjectures bound this number in terms of the multidegree and the volume of the Newton polytope of a polynomial defining the hypersurface, respectively.In the second part of the thesis, we present an upper bound for the height of isolated zeros, in the torus, of a system of Laurent polynomials over an adelic field satisfying the product formula. This upper bound is expressed in terms of the mixed integrals of the local roof functions associated to the chosen height function and to the system of Laurent polynomials. We also show that this bound is close to optimal in some families of examples. This result is an arithmetic analogue of the classical Bern\v{s}tein-Ku\v{s}nirenko theorem.

Cette thèse porte sur l'alignement automatique d'un enregistrement audio avec la partition de musique correspondante. Nous adoptons une approche probabiliste et proposons une démarche théorique pour la modélisation algorithmique de ce problème d'alignement automatique. La question est de modéliser l'évolution temporelle des événements par des processus stochastiques. Notre démarche part d'une spécificité de l'alignement musical : une partition attribue à chaque événement une durée nominale, qui est une information a priori sur la durée probable d'occurrence de l'événement. La problématique qui nous occupe est celle de la modélisation probabiliste de cette information de durée. Nous définissons la notion de cohérence temporelle à travers plusieurs critères de cohérence que devrait respecter tout algorithme d'alignement musical. Ensuite, nous menons une démarche axiomatique autour du cas des modèles de semi-Markov cachés. Nous démontrons que ces critères sont respectés lorsque des conditions mathématiques particulières sont vérifiées par les lois a priori du modèle probabiliste de la partition. Ces conditions proviennent de deux domaines mathématiques jusqu'ici étrangers à la question de l'alignement : les processus de Lévy et la totale positivité d'ordre deux. De nouveaux résultats théoriques sont démontrés sur l'interrelation entre ces deux notions. En outre, les bienfaits pratiques de ces résultats théoriques sont démontrés expérimentalement sur des algorithmes d'alignement en temps réel. / This thesis deals with automatic alignment of audio recordings with corresponding music scores. We study algorithmic solutions for this problem in the framework of probabilistic models which represent hidden evolution on the music score as stochastic process. We begin this work by investigating theoretical foundations of the design of such models. To do so, we undertake an axiomatic approach which is based on an application peculiarity: music scores provide nominal duration for each event, which is a hint for the actual and unknown duration. Thus, modeling this specific temporal structure through stochastic processes is our main problematic. We define temporal coherency as compliance with such prior information and refine this abstract notion by stating two criteria of coherency. Focusing on hidden semi-Markov models, we demonstrate that coherency is guaranteed by specific mathematical conditions on the probabilistic design and that fulfilling these prescriptions significantly improves precision of alignment algorithms. Such conditions are derived by combining two fields of mathematics, Lévy processes and total positivity of order 2. This is why the second part of this work is a theoretical investigation which extends existing results in the related literature.

Dans cette thèse, nous abordons deux problèmes de théorie des graphes liés à deux problèmes biologiques de symbiose (deux organismes vivent en symbiose s'ils ont une interaction étroite et à long terme). Le premier problème est lié au phénomène de l'Incompatibilité cytoplasmique (IC) induit par certaines bactéries parasites chez leurs hôtes. L'IC se traduit par l'impossibilité de donner naissance à une progéniture saine lorsqu'un mâle infecté s'accouple avec une femelle non infectée. En termes de graphe ce problème peut s'interpréter comme la recherche d'une couverture minimum par des "sous-graphes des chaînes" d'un graphe biparti. Un graphe des chaînes est un graphe biparti dont les noeuds peuvent être ordonnés selon leur voisinage.En terme biologique, la taille minimale représente le nombre de facteurs génétiques impliqués dans le phénomène de l'IC. Dans la première moitié de la thèse, nous abordons trois problèmes connexes à ce modèle de la théorie des graphes. Le premier est l'énumération de tous les graphes des chaînes maximaux arêtes induits d'un graphe biparti G, pour lequel nous fournissons un algorithme en delai polynomial avec un retard de O(n^2m) où n est le nombre de noeuds et m le nombre d'arêtes de G. Dans la même section, nous montrons que (n/2)! et 2^(\sqrt{m}\log m) bornent le nombre de sous-graphes de chaînes maximales de G et nous les utilisons pour établir la complexité "input-sensitive" de notre algorithme. Le deuxième problème que nous traitons est de trouver le nombre minimum de graphes des chaînes nécessaires pour couvrir tous les bords d'un graphe biparti.Pour résoudre ce problème NP-hard, en combinant notre algorithme avec la technique d'inclusion-exclusion, nous fournissons un algorithme exponentiel exact en O^*((2+c)^m), pour chaque c > 0 (par O^* on entend la notation O standard mais en omettant les facteurs polynomiaux). Le troisième problème est l'énumération de toutes les couvertures minimales par des sous-graphes des chaînes. Nous montrons qu'il est possible d'énumérer toutes les couvertures minimales de G en temps O([(M + 1) |S|] ^ [\ log ((M + 1) |S|)]) où S est le nombre de couvertures minimales de G et M le nombre maximum des sous-graphes des chaînes dans une couverture minimale. Nous présentons ensuite la relation entre le second problème et le calcul de la dimension intervallaire d'un poset biparti. Nous donnons une interprétation de nos résultats dans le contexte de la dimension d'ordre / In this thesis, we address two graph theoretical problems connected to two different biological problems both related to symbiosis (two organisms live in symbiosis if they have a close and long term interaction). The first problem is related to the size of a minimum cover by "chain subgraphs" of a bipartite graph. A chain graph is a bipartite graph whose nodes can be ordered by neighbourhood inclusion. In biological terms, the size of a minimum cover by chain subgraphs represents the number of genetic factors involved in the phenomenon of Cytoplasmic Incompatibility (CI) induced by some parasitic bacteria in their insect hosts. CI results in the impossibility to give birth to an healthy offspring when an infected male mates with an uninfected female. In the first half of the thesis we address three related problems. One is the enumeration of all the maximal edge induced chain subgraphs of a bipartite graph G, for which we provide a polynomial delay algorithm with a delay of O(n^2m) where n is the number of nodes and m the number of edges of G. Furthermore, we show that (n/2)! and 2^(\sqrt{m} \log m) bound the number of maximal chain subgraphs of G and use them to establish the input-sensitive complexity of the algorithm. The second problem we treat is finding the minimum number of chain subgraphs needed to cover all the edges of a bipartite graph. To solve this NP-hard problem, we provide an exact exponential algorithm which runs in time O^*((2+c)^m), for every c>0, by a procedure which uses our algorithm and an inclusion-exclusion technique (by O^* we denote standard big O notation but omitting polynomial factors). Notice that, since a cover by chain subgraphs is a family of subsets of edges, the existence of an algorithm whose complexity is close to 2^m is not obvious. Indeed, the basic search space would have size 2^(2^m), which corresponds to all families of subsets of edges of a graph on $m$ edges. The third problem is the enumeration of all minimal covers by chain sugbgraphs. We show that it is possible to enumerate all such minimal covers of G in time O([(M+1)|S|]^[\log((M+1)|S|)]) where S is the number of minimal covers of G and M the maximum number of chain graphs in a minimal cover. We then present the relation between the second problem and the computation of the interval order dimension of a bipartite poset. We give an interpretation of our results in the context of poset and interval poset dimension... [etc]