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'').
La complexité de l'étude formelle des protocoles cryptographique se situe à plusieurs niveaux. Il faut d'abord modéliser les communications qui ont lieu entre les participants, puis définir précisément les propriétés que l'on souhaite vérifier. Celles-ci peuvent être assez simples à exprimer, comme les propriétés de secret, ou très complexes, comme les propriétés de résistance à la coercition dans les protocoles de vote. Le pi-calcul appliqué est de plus en plus utilisé pour formaliser des protocoles cryptographiques. Il étend le pi-calcul traditionnel en permettant aux processus de manipuler aisément des termes dotés d'une théorie équationnelle. On peut par exemple y inclure des primitives pour le chiffrement ou la signature de message, la création de paires de clés privées/publiques, ou toute autre fonction utile pour le protocole à formaliser. Différentes équivalences permettent ensuite de comparer les processus, dont l'équivalence statique qui, intuitivement, exprime ce qu'un attaquant peut déduire d'un protocole à une étape donnée de son exécution. Pour écrire les propriétés à vérifier sur ces protocoles, on a usuellement recours à différentes logiques, telles que les logiques de Hennessy Milner, de Cardelli-Gordon, et de Caires. L'une de ces logiques est la logique spatiale, qui permet de décrire non seulement les communications dont est capable un processus, mais aussi leur localisation au sein de celui-ci. Ceci permet par exemple de distinguer les différents participants d'un protocole. Cette logique apparaît donc comme un point de départ pertinent pour l'étude de protocoles cryptographique. Le but de ce travail était d'adapter la logique spatiale au traitement du pi-calcul appliqué et d'étudier son expressivité, notamment en termes de propriétés de secrets, sécurité, déductibilité, etc. Nous introduirons tout d'abord la logique spatiale du pi-calcul appliqué que nous avons définie, avant de présenter les résultats théoriques d'expressivité obtenus dans ce nouveau cadre (intensionalité, élimination des quantificateurs, ...), qui rejoignent ceux déjà connus pour le pi-calcul. Enfin, nous donnerons quelques intuitions concernant les propriétés de sécurité et de secret qu'il est possible d'exprimer au sein de la logique, notamment en donnant des formules qui caractérisent l'équivalence statique.
On établit une formule pour la courbure de Gauss-Bonnet-Chern totale d'un ensemble semi-algébrique fermé X de R^n en fonction de sa caractéristique d'Euler-Poincaré et de son comportement à l'infini.
Dans cet exposé, nous démontrerons le résultat d'indécidabilité obtenu par R. Berger en 1964 sur les pavages : savoir, étant donné un jeu fini de tuiles de Wang, s'il existe un pavage valide du plan par ces tuiles est indécidable. Après une brève discussion sur différentes façons de définir des jeux de tuiles et les pavages du plan engendrés, nous nous intéresserons à la problématique de l'apériodicité, introduite par H. Wang. Dans l'esprit des constructions originelles de R. Berger et R. M. Robinson, nous construirons un jeu de tuiles apériodique et nous montrerons comment ce jeu de tuiles peut être étendu pour générer les pavages limites de n'importe quelle substitution 2x2. Fort de cette construction, nous pourrons calculer dans les pavages et obtenir les résultats d'indécidabilité annoncés.
In this talk, I will present our work in which we are trying to make a connection between formal and natural languages. We aim to develop tools and resources capable of translating between natural languages and formal languages. I will present our attempts in translating mathematical proofs written in natural language into formal proofs. The implementation of our work is based on the Grammatical Framework (GF). GF is a grammar formalism based on type theory, which provides a special purpose language for defining grammars, and a compiler for this language. Further I will give an overview of the future work i.e. Checking formal software specifications with the specifications written in a natural language and to validate whether they correspond to each other or not. I will also argue that it is a very hard problem to generate a good quality text from a formalism. A natural motivation for this work is the fact that it is a normal practice in industry to write specifications in natural language. In a similar way, all the standards such as RFCs, ISO, ANSI, patents are written in plain natural language. Therefore this resource has an immediate usability in the industry. It will help to overcome the difficulties that prevent software designers & engineers to use formal methods. This Project has its usefulness in formal methods, Human computer interaction, natural language technology and Mathematical teaching.
Cet exposé traite de l'évolution quasi-statique de fissures dans des films minces fragiles obéissant au critère de Griffith. Le point de départ est un cylindre tridimensionnel d'épaisseur arbitrairement petite. L'existence d'une évolution quasi-statique du modèle de Francfort-Marigo a été démontrée par Dal Maso-Francfort-Toader et l'on cherche à savoir comment celle-ci se comporte lorsque l'épaisseur du film tend vers zéro. Tout d'abord, le problème statique sera présenté au moyen d'une analyse par Gamma-convergence avec une énergie de surface ne donnant pas de compacité dans l'espace SBV des fonctions spéciales à variation bornée. Il sera démontré que l'énergie de surface limite (bidimensionnelle) est toujours de type Griffith et que l'énergie de volume est la même que celle obtenue par Le Dret-Raoult dans les espaces de Sobolev. Ensuite, l'analyse asymptotique de l'évolution quasi-statique sera présentée dans le cas de solutions uniformément bornées. En particulier, il sera démontré qu'elle converge en un certain sens vers une évolution quasi-statique associée au modèle Gamma-limite.
Inspired by the unanswered question: why eukariotic DNA has a so large non-coding fraction, we try computer simulations with an evolutionary toy model based on Turing machines. This lead us to describe how the fitness of an ``organism'' and the evolution rate relate to the coding/non-coding ratio. The evolutionary advantage of having a large reservoir of non-coding states is emphasised.
En 2004, G. Gonthier a achevé la preuve formelle du théorèmes de quatre couleurs dans l'assistant à la preuve Coq. L'une des clefs de cette réussite est une utilisation intensive de techniques dites de ``réflexion à petite échelle'', soutenues par une extension du langage de tactiques de Coq. Cette extension, ainsi qu'une partie des bibliothèques développées pour la preuve, sont actuellement utilisées comme point de départ pour le projet de formalisation d'une somme substantielle de théorie des groupes finis, dans l'équipe Composants Mathématiques du centre commun INRIA MSR. Il s'agit cette fois de construire une preuve formelle du théorème de Feit-Thompson (1963), qui constitue un passage a l'échelle significatif pour les contributions issues de la preuve du théorèmes des quatre couleurs. Le but de cette expérience est de comprendre comment mener à bien le développement de bibliothèques de mathématiques formalisées, réutilisables et combinables. Nous tenterons d'abord de dégager les difficultés que présente la réalisation de telles bibliothèques, puis de présenter les solutions qui se dégagent de la preuve du théorème des quatre couleurs, et en particulier le langage de tactiques ssreflect. Enfin, si le temps le permet, nous présenterons brièvement les nouvelles questions soulevées par la formalisation de théorie des groupes finis, ainsi que l'état actuel de cette construction.
Nous donnons plusieurs généralisations du théorème suivant de Clarke, (sur l'inversion locale des fonctions lipschitziennes) : soit $f$ une fonction d'un ouvert de $R^n$ dans $R^n$ si l'enveloppe convexe fermée des limites (en un point $x$) des différentielles ne contient pas des matrices singulières alors $f$ est inversible au voisinage de $x$. Nos résultats concernent essentiellement le cas des fonctions définissables dans une structure o-minimale. La preuve du résultat principal utilise quelques notions d'analyse convexe. La généralisation au cas de dimension infinie reste largement ouverte.
Pierre Hyvernat (LAMA) prendra environ 1/2h pour poser une question sur laquelle il bute actuellement. Ensuite, séance lecture sur le papier de Krivine et Legrandgérard, téléchargeable ici:
http://www.pps.jussieu.fr/ krivine/articles/Network.pdf.
Résumé du papier: On décrit une relation remarquable entre la notion de formule valide du calcul des prédicats et la spécification de protocoles réseau. On donne des exemples comme l'acquittement d'un ou plusieurs paquets.
In the talk I discuss the crack initiation problem in a hyper-elastic body governed by a Griffith's type energy. The main tool employed to address the problem is a local minimality result for a free discontinuity functional F involving bulk and surface energies: under general assumptions concerning the shapes of the admissible cracks, the uncracked configuration turns out to be a local minimizer of F.
Soit X une surface algébrique réelle connexe compacte rationnelle non-singulière. Notons Diff_alg(X) le groupe des difféomorphismes algébriques de X dans X. Le groupe Diff_alg(X) agit diagonalement sur X^n pour tout entier naturel n. Nous montrons que cette action est transitive pour tout n. Comme application, nous donnons une nouvelle preuve plus simple du fait que deux surfaces algébriques réelles connexes compactes rationnelles non-singulières sont algébriquement difféomorphes si et seulement si elles sont homéomorphes en tant que surfaces topologiques.
Nous proposons une extension du lambda-calcul traditionel dans lequel les termes sont utilisés pour manipuler un artefact de calcul externe (bits quantiques, brins d'ADN etc.). Nous introduisons deux nouveaux lieurs de noms : $nu$ et $rho$. $new x.M$ dénote un terme dans lequel $x$ est une référence abstraite, alors que dans $rho y.M$, $y$ est une référence conrète. Nous montrons les différences de ces deux lieurs par rapport au $lambda$ en termes d'$alpha$ équivalence, d'extrusion, de garbage collection etc. Nous illustrons l'intérêt de ces nouveaux lieurs en développant un langage de programmation quantique typé dans lequel la duplication de qbits abstrait est permise alors que la duplication de qbits concrets est interdite. Cela permet un langage plus expressif que ceux proposés dans la littérature actuelle.
Urdu is a challenging language because of, first, its Perso-Arabic script and second, its morphological system having inherent grammatical forms and vocabulary of Arabic, Persian and the native languages of South Asia. This paper describes an implementation of the Urdu language as a software API, and we deal with orthography, morphology and the extraction of the lexicon. The morphology is implemented in a toolkit called Functional Morphology, which is based on the idea of dealing grammars as software libraries. Therefore this implementation could be reused in applications such as intelligent search of keywords, language training and infrastructure for syntax. We also present an implementation of a small part of Urdu syntax to demonstrate this re-usability.