Dans les années quatre-vingt-dix, on a remarqué ce que l'isomorphisme de Curry-Howard peut être étendu à la logique classique. De nombreux calculs ont été développés pour constituer la base de cette extension. On étudie dans cette thèse quelques uns de ces calculs.
On étudie tout d’abord le lambda-mu-calcul simplement typé de Parigot. Parigot a prouvé par des méthodes sémantiques que son calcul est fortement normalisable. Ensuite, David et Nour ont donné une preuve arithmétique de la normalisation forte de ce calcul avec la règle mu' (règle duale de mu). Cependant, si l'on ajoute au lambda-mu-mu'-calcul la règle de simplification rho, la normalisation forte est perdue. On monte que le mu-mu'-rho-calcul non-typé est faiblement normalisable et que le lambda-mu-mu'-rho-calcul typé est aussi faiblement normalisable. De plus, on examine les effets d'ajouter quelques autres règles de simplification. On établit ensuite une borne de la longueur des séquences de réduction en lambda-mu-rho-theta-calcul simplement typé. Ce résultat est une extension de celui de Xi pour le lambda-calcul simplement typé. Enfin, on présente une preuve arithmétique de la normalisation forte du lambda-calcul symétrique de Berardi et Barbanera.
Des familles inductives de types de données servent bien à représenter le lambda-calcul: le paramètre de la famille décrit l'ensemble de noms de variables libres admises, et le changement du paramètre au cours de la récurrence reflète la génération de noms pour les variables liées. Cette représentation satisfait les propriétés de base de la substitution, dictées par la théorie des catégories. C'est bien connu.
On veut aller plus loin: On encapsule des sous-expressions de lambda-termes comme si elles n'étaient que des noms de variables libres. Ceci donne le lambda-calcul avec aplatissement explicite (une forme de substitution explicite). Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont offertes par aucun assistant de preuves, or elles pouvaient être encodées dans Coq. Là, déjà la notion d'une occurrence libre d'une variable est un défi pour la conception mathématique.
Heureusement, la vérification entière se fait dans Coq, le plus grand problème étant un affaiblissement de la règle que la substitution qui remplace chaque variable par le terme qui consiste de cette variable n'a aucun effet. En plus, toute notre théorie axiomatique est justifiée dans le calcul des constructions inductives avec insignifiance des preuves.
Ce texte de synthèse a pour but de présenter l'évolution de mes recherches postèrieures à ma thèse. Ce travail s'articule autour de plusieurs axes de recherche dans le cadre des équations aux dérivées partielles non linéaires et en particulier des lois de conservation. Il s'inscrit dans l'étude des problèmes hyperboliques, des problèmes mixtes et des équations cinétiques. Les domaines d'application sont la mécanique des fluides ou du solide, la propagation de composants chimiques, l'électromagnétisme, l'optique. Mon activité concerne d'abord la modélisation de phénomènes physiques ou chimiques sous forme d'équations aux dérivées partielles non linéaires telles que les équations de Bloch, Korteweg, Navier-Stokes, Saint-Venant, puis vient l'étude mathématique de ces équations à travers les problèmes d'existence, d'unicité, de régularité avec éventuellement la mise au point de méthodes numériques de résolution. Ce document est divisé en une introduction générale et trois chapitres qui concernent respectivement les systèmes hyperboliques avec conditions aux limites et la chromatographie, les problèmes d'analyse asymptotique et enfin les méthodes cinétiques. Dans chaque partie, un historique et une présentation des différents résultats mathématiques sont faits et quelques problèmes ouverts sont donnés.
Dans cet exposé, on présentera des bornes sur la topologie d'un hypersurface fewnomiale qui améliorent grandement celles précédemment connues. Ces nouvelles bornes utilisent celles obtenues récémment par l'orateur et Frank Sottile sur le nombre de solutions positives de systèmes fewnomiaux. On montrera aussi, si le temps le permet, comment on peut modifier légèrement la preuve de de ces dernières bornes de manière à en obtenir d'autres sur le nombre de solutions réelles, qui soient également asymptotiquement optimales.
We introduce a new curvature estimator based on global optimisation. This method called Global Min-Curvature exploits the geometric properties of digital contours by using local bounds on tangent directions defined by the maximal digital straight segments. The estimator is adapted to noisy contours by replacing maximal segments with maximal blurred digital straight segments. Experimentations on perfect and damaged digital contours are performed and in both cases, comparisons with other existing methods are presented.
Dans une première partie, nous présentons des équations de Saint-Venant. Sur le modèle proprement dit, nous remarquons tout d'abord que, suivant le lien entre la viscosité et le rapport d'aspect, il est indispensable de conserver l'expression complète de la force de Coriolis : nous obtenons ainsi un nouveau modèle, avec un ``effet cosinus''. Nous montrons alors que les preuves d'existence de solutions faibles peuvent être adaptées à ce nouveau système. Des simulations numériques de certaines ondes soulignent l'importance de ce terme. Nous étudions ensuite l'influence des conditions limites (surface, fond) et du tenseur des contraintes sur des modèles de type Saint-Venant. Nous présentons également des modèles obtenus en utilisant des échelles multiples en espace et en temps. Enfin, nous analysons théoriquement et numériquement un nouveau modèle de sédimentation puis nous donnons certains résultats pour les fluides visco-plastiques. Dans une deuxième partie, nous nous intéressons aux équations limites que sont les équations quasi-géostrophiques (QG) et les équations des lacs. L'étude numérique des équations QG 2d met en évidence le rôle de l'effet cosinus de la force de Coriolis. En fonction de la topographie considérée, nous montrons que celui-ci peut être non négligeable. Toujours sur les équations QG, nous donnons un schéma, basé sur des développements asymptotiques, qui permet de bien capter la couche limite mais aussi d'ajouter le terme de topographie à la solution obtenue avec fond plat, sans tout recalculer. Enfin, nous expliquons l'obtention des équations des lacs avec effet cosinus, et nous prouvons que les propriétés d'existence de solutions restent valables.
Les axiomes d'o-minimalité les plus généraux ne spécifient pas qu'une structure o-minimale définit une structure de corps réel clos sur son univers. Néanmoins, le théorème de trichotomie assure qu'il est difficile de ne pas y trouver un corps: à moins qu'une structure o-minimale soit triviale'' oulocalement modulaire'', un corps y est type-définissable. Dans le cas où la structure a pour univers l'ensemble des réels muni de son ordre naturel et définit le graphe de l'addition, et qu'elle est ni triviale ni localement modulaire, il se peut que la structure de corps découlant du théorème de trichotomie ne soit pas la structure naturelle de corps des réels. Nous présenterons quelques critères assurant que ce soit bien le cas.
We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor---a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow constructs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics. Using our modularity principle, we proved the sequential CSL rules (those that are inherited from sequential Separation Logic) simply by adapting Appel & Blazy's machine-checked sequential-separation-logic soundness proofs with minimal changes. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimizing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent setting. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine.
D’après un théorème célèbre énoncé par Comessatti en 1914, si X est une surface géométriquement rationnelle et définie sur R, alors une composante connexe orientable S de X a son genre g(S) majoré par 1. Ce résultat reste vrai si on considère plus généralement X uniréglée. En dimension trois, le genre ne suffit plus à classifier les variétés compactes orientables et la classe des variétés uniréglées est plus vaste. Nous discuterons des généralisations possibles en dimension trois de l’énoncé de Comessatti à la lumière de plusieurs résultats récents de Kollár, Viterbo, Eliashberg, Huisman, Catanese et moi-même.
Une manière de stocker de manière économe un gros objet géométrique discret (images 3D acquises expérimentalement etc.) est de le vectoriser. Une façon de procéder est de le décomposer en plans discrets (approximations de plans euclidiens). Pour cela, un problème crucial est celui de la reconnaissance de plan : déterminer si un ensemble discret est ou non inclus dans un plan discret. Nous présentons une approche originale, qui généralise une approche similaire pour le cas de la reconnaissance de droites. Plus précisément, on montre comment calculer un développement en fraction continues multi-dimensionnel du vecteur normal d'un plan discret simplement en lisant les configurations locales de ce plan. Ce procédé peut alors être étendu à des ensembles discrets plus généraux, bien qu'ils n'aient pas forcément de vecteur normal. Les développements de plans possèdent cependant des propriétés qui permettent finalement de les reconnaître.
Un résultat classique sur les structures o-minimales affirme que tout ensemble définissable est, pour tout entier $k$, une union finie de cellules de classe $C^k$. En fait, la plupart des structures o-minimales connues ont la propriété de décomposition cellulaire analytique. Dans un travail récent en commun avec Olivier Legal (Université de Rennes), nous montrons comment construire, à partir d’algèbres quasianalytiques convenables, une structure o-minimale qui n’admet pas la propriété de décomposition cellulaire $C^{\infty}$.
La correspondance de Curry-Howard permet d'interpréter chaque démonstration mathématique comme un programme réalisant une certaine spécification (déduite de la formule démontrée). Mais que se passe-t-il quand la démonstration fait appel à des hypothèses expérimentales - par exemple des lois de la physique?
Dans cet exposé, je me propose d'étudier la frontière entre le raisonnement mathématique et les hypothèses empiriques sur lesquelles reposent les sciences expérimentales. Pour cela, je partirai d'un problème soulevé par le philosophe et épistémologue Karl R. Popper lié à l'utilisation des formalismes mathématiques les plus abstraits dans un cadre empirique. Je montrerai alors comment les techniques modernes de réalisabilité permettent de résoudre ce problème, et suggèrent ainsi des pistes inédites pour combiner de manière effective le raisonnement mathématique avec les protocoles expérimentaux.