CoqHoTT: Coq for Homotopy Type Theory

The goal of this project is to go further in the correspondence between proofs and programs which has allowed in the last 20 years the development of useful proof assistants, such as Coq (developed by Inria). Those assistants have shown their efficiency to prove correctness of important pieces of software but their democratization suffers from a major drawback, the mismatch between equality in mathematics and in type theory (which is the theory at the heart of Coq). Thus, significant Coq developments have only been done by virtuosos playing with advanced concepts of both computer science and mathematics. Recently, an extension of type theory with homotopical concepts has been proposed by field medal Vladimir Voevosdky, which allows for the first time to get the right notion of equality in theorem provers. The main goal of the CoqHoTT project is to provide a new generation of proof assistants based on this fascinating connection between homotopy theory and type theory.

In this talk, I will spend a long time presenting the basics of Type Theory and Homotopy Type Theory and try to present quickly the main goal of the CoqHoTT project.

Dans cet exposé on décrira un invariant de sous-variétés legendriennes, l'homologie de contact legendrienne, définie en associant à une sous-variété legendrienne L une algèbre différentielle graduée, l'algèbre de Chekanov, engendrée par les cordes de Reeb de L. En dimension 3, la théorie est entièrement combinatoire et dans ce cas là on donnera des idées de la preuve de l'invariance par isotopie legendrienne de cette homologie. Une version linéarisée fournit ensuite un invariant plus calculable, qui a permis à Chekanov de mettre en évidence l'exemple de deux nœuds legendriens de mêmes invariants classiques qui ne sont pour autant pas isotopes. En fonction du temps on verra comment se généralisent ces notions en dimension plus grande que 3.

Les équations cinétiques collisionnelles, donc le prototype est l'équation de Boltzmann, décrivent de manière bien plus précise que des équations fluides de nombreux phénomènes physiques ou biologiques comme les gaz raréfiés, les milieux granulaires ou les bancs de poisson. Néanmoins, en raison d'un espace des phases de grande dimension, il est très couteux d'effectuer des simulations numériques pour ce type d'équations. Dans ce travail en collaboration avec F. Filbet et K. Aoki, nous construisons une hiérarchie de méthodes numériques hybrides cinétique/fluide pour ce type d'équations multi-échelles. Notre approche est basée sur le concept de matrice de réalisabilité des moments, introduit par Levermore, Morokoff and Nadiga. Cela nous permet de considérer des modèles hybrides où la partie fluide peut être donnée par les équations d'Euler, de Navier-Stokes, ou même de Burnett et super-Burnett. Le gain de temps de calcul rend notre méthode compétitive avec des modèles fluides, tout en gardant la précision d'un modèle cinétique.

On s'intéresse ici à l'approximation du problème de Stokes 2D par la méthode Discrete Duality Finite Volume (DDFV). Cette méthode de volumes finis (qui généralise le schéma MAC) a notamment pour avantages de pouvoir s'adapter aisément à des maillages quelconques ou à des écoulements bi-fluides, tout en conservant au plan discret les propriétés principales des opérateurs différentiels mis en jeu. Plus précisément, on étudie d'un point de vue théorique et numérique la stabilité Inf-Sup de ce schéma pour différents types de maillages, en particulier non conformes.

Cet exposé a pour but de proposer une introduction à la théorie de Morse. La principale question abordée sera la suivante : étant connue une fonction définie sur une variété M, peut-on en déduire des informations sur la structure de la variété elle-même ? La réponse est généralement oui : la donnée d'une fonction de Morse induit une structure de complexe cellulaire sur M. On présentera les grandes idées de la preuve de ce résultat. Si le temps le permet, on abordera également les questions de réarrangement et d'annulation de points critiques.