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.
Il s'agit d'un travail en collaboraion avec Gérard Philippin de l'Université Laval à Québec. Dans cet exposé, nous nous intéressons au produit de moment d'inertie sur un domaine, ainsi que des moments d'inertie sur le bord d'un domaine. Dans chacun des cas, nous cherchons quels sont les domaines du plan d'aire fixée qui minimise ces produits. Nous montrerons également comment ce travail est connecté à une inégalité isopérimétrique satisfaite par les premières valeurs propres de l'opérateur de Stekloff.
La mécanique classique nous parvient des équations différentielles sous la forme : $\frac{dX}{dt}=f(X)$, $t\in \mathbb{R}$, $X\in \mathbb R^n$. Normalement, il y a très peu choses qu’on sait dire sur la dynamique globale des solutions $X(t)$ vues comme des courbes réelles dans $\mathbb{R}^n$. L’étude s’enrichit beaucoup quand on complexifie le problème i.e considère $t\in \mathbb{C}$, $X\in \mathbb C^n$. L’approche de Ziglin (1980’s) réduit alors l’analyse des propriétés dynamiques (l’intégrabilité, la stabilité etc.) à l’étude purement algébrique des sous-groupes de $\mathrm{GL}(n,\mathbb{C})$ qui apparaissent comme des groupes de monodromie des équations aux variations autour d’une solution particulière. Dans cette exposé je présente des résultats récents dans cette direction relatives aux problèmes classiques da la mécanique : le problème des trois corps, le Rattleback et le Levitron (une toupie flottant dans le champ magnétique). Quelques démonstrations sont prévues. Références [1] A. Tsygvintsev, On some exceptional cases in the integrability of the three-body problem, Celestial Mechanics and Dynamical Astronomy, Vol. 99, No. 1, 237-247, 2007 [2] H. Dullin, A. Tsygvintsev, On the analytic non-integrability of the Rattleback problem, Annales de la faculté des sciences de Toulouse, à paraître
A gentle introduction to categorical models of dependent type theory. As a warm up, Richard will explain the interpretation in locally cartesian closed categories (LCCCs), and why it necessarily leads to extensional models of type theory. Then, he will, rather informally, try to explain why models of intensional type theory should look like weak omega categories (read the ordinal ``omega'').