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.
Je présente la preuve de Prawitz de la faible normalisation de l'élimination des coupures en déduction naturelle propositionnelle intuitionniste avec disjonction. On déduit ensuite la propriété de la sous-formule et la décidabilité de ce système. Il s'agit du travail fait lors de mon stage M1.
On présentera (il s'agit d'un travail commun avec Olivier Laurent) une version "pure" (au sens du lambda-calcul "pur") des réseaux d'interaction différentiels avec connecteurs multiplicatifs et exponentiels, et on donnera une traduction dans ces réseaux du pi-calcul privé - de la somme - de la récursion - de la réplication - du match et du mismatch On verra que cette traduction respecte, en un certain sens, la dynamique du pi-calcul.
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. La preuve que cette représentation satisfait les propriétés de base de la substitution - dictées par la théorie de catégories - n'est pas triviale et un travail assez récent (pour Coq, c'était fait par Adams). 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. Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont pas 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 des propriétés de base était abordable 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.