. Nous allons introduire les outils de cohomologie $p$-adique utilisés par Kedlaya dans son algorithme pour calculer le nombre de points d'une courbe hyperelliptique sur un corps fini de petite caractéristique.
l
Cette thèse traite de logique, sous la forme de la théorie des types ou logique d'ordre supérieur, et de calcul, sous la forme de récriture, un paradigme de calcul
Turing-complet, c'est-à-dire, par lequel on peut exprimer toutes les fonctions calculables.
Une démonstration mathématique est généralement constituée de raisonnements ingénieux et de calculs mécanisables. Or les systèmes de développement de
preuves actuels (Coq, Lego, Nuprl, HOL, etc.) ont un mécanisme de calcul assez rudimentaire. Bien qu'ils permettent d'exprimer de très nombreuses fonctions
(toute fonction dont l'existence est prouvable en arithmétique intuitionniste d'ordre supérieur), les définitions peuvent être malaisées et parfois inefficaces (celles-ci
doivent suivre un schéma très restrictif semblable à la récursion primitive). Ces systèmes ne permettent donc pas de définir fonctions et prédicats de la manière que
l'on veut, ce qui les rend difficiles à utiliser par des non-spécialistes et limite l'aspect ``calcul'': des propositions qui pourraient être prouvées de manière
automatique, par un simple calcul, nécessitent des déductions compliquées. Inversement, avec une notion de calcul plus riche mais telle que l'égalité de deux
termes soit décidable, il n'est pas nécessaire de mémoriser les étapes de calcul. Les preuves se trouvent ainsi réduites aux ``raisonnements''. Or, actuellement, la
taille des preuves est un problème critique dans les systèmes de développement de preuves.
Les définitions à l'aide de règles de récriture sont à la fois plus générales, plus aisées et peuvent être plus efficaces. Mais considérer des fonctions ou des prédicats
définis par un ensemble de règles de récriture a priori quelconques pose un problème essentiel: peut-on vérifier si une preuve est correcte ou non ? C'est la
``décidabilité du typage''. Ce problème est difficile car, pour vérifier qu'une preuve est correcte, on doit être capable de décider si deux termes sont égaux modulo la
récriture. Pour cela, il est nécessaire que la récriture soit:
confluente: l'ordre des récritures n'a pas d'importance,
fortement normalisante: un terme ne peut pas être récrit
indéfiniment.
Il existe de nombreux résultats sur la confluence et la normalisation forte de la récriture dite du premier ordre, c'est-à-dire, s'appliquant aux termes d'une algèbre
engendrée par un ensemble de symboles et un ensemble de variables. Mais, dans le cadre du Calcul des Constructions de T. Coquand et G. Huet, un système de
types dépendants et polymorphes qui permet d'exprimer les propositions et les preuves de la logique d'ordre supérieur et qui généralise le lambda-calcul
polymorphe de J.-Y. Girard, on peut vouloir définir des fonctions polymorphes d'ordre supérieur, c'est-à-dire, paramétrées par des types et des fonctions comme,
par exemple, une fonction de tri paramétrée par le type des éléments à trier et une fonction de comparaison sur ce type. Cela permet d'écrire des programmes
génériques, une propriété importante en génie logiciel.
Or, il existe très peu de résultats sur la confluence et la normalisation forte de ce type de récriture. De plus, jusqu'à maintenant, aucun travail n'a considéré une
telle forme de récriture au niveau des types et des prédicats (seul le Calcul des Constructions Inductives autorise la définition de prédicats par récurrence, une
forme très restreinte de récriture). Pourtant, la récriture au niveau des types permet d'augmenter la puissance logique du formalisme et aussi de formaliser des
procédures de décision.
Dans notre thèse, nous commençons par étudier les propriétés des Systèmes de Types Purs, une classe très générale de systèmes de types dont fait partie le Calcul
des Constructions, quand ceux-ci sont étendus par de la récriture. En particulier, nous montrons qu'il est possible de linéariser certaines règles de récriture (une
règle de récriture est linéaire si une variable n'apparaît pas deux fois dans le membre gauche) sans mettre en péril la préservation du typage ou la normalisation
forte. Cela a deux conséquences pratiques importantes: puisqu'il n'y a pas de tests d'égalité pour appliquer une règle, d'une part, la récriture est plus efficace et,
d'autre part, la confluence est bien plus facile à montrer.
Ensuite, pour assurer la confluence et la normalisation forte dans le cas du Calcul des Constructions, nous donnons des conditions très générales sur les règles de
récriture dont la vérification peut être automatisée. Celles-ci généralisent tous les résultats antérieurs sur la combinaison Calcul des Constructions et récriture, y
compris le Calcul des Constructions Inductives. Nous montrons également que ces conditions peuvent s'appliquer à la Déduction Naturelle Modulo.
Bien sûr, ces conditions peuvent encore être généralisées. Par exemple, nous n'avons pas considérer de récriture modulo certaines théories équationnelles comme
l'associativité ou la commutativité, très utiles en pratique. Et des restrictions trop importantes pèsent sur les règles au niveau des types. Par ailleurs, nous n'avons
pas abordé le problème de la cohérence logique qui, déjà, en l'absence de récriture, n'admet pas de solution générale. Tous ces problèmes font partie de nos projets
de recherche.
l We shall consider the physical layer of mobile communications, i.e. one link between a Base Station (in GSM, Node-B in UMTS) and a mobile station (User Equipment (UE) in UMTS). An important measure for the analysis of this link's performance is the probability that a bit is decoded incorrectly at reception, otherwise called Bit Error Rate (BER). A classical formula due to Barret ('87) giving a closed form of this probability is computationaly unstable in some cases that reflect some real-life situations. Rewriting it in a such a way that it becomes stable, one obtains an expression containing certain symmetric functions. Their decomposition in the base of Schur functions gives rise to a set of interesting combinatorial objects (combinations of Young tableaux). Those in turn can be bijectively mapped to sets of 0-1 matrices that yield easier to analysis and allow to obtain stable closed form expressions for the probability in question in several cases where Barret's formula fails to do so.
l The operational semantics of many computational systems can often be encoded as logical theories. One of the main issues in the encoding is in finding a logical treatment of variable-binding constructs in the specifications of computational systems. In our current approach, variable-bindings in the specifications are encoded as term-level abstractions (lambda-abstraction) in the logic, which means that generic judgments are generally required to reason about the properties of the encoded specifications. Term-level abstractions are then given operational meaning using proof-level abstractions (eigenvariables). However, if the logical system is a traditional sequent system, different kinds of binding constructs are identified at the proof-level, which may not be appropriate for certain computational systems. Dale Miller and I have recently designed a new logical system which has for a richer structure of proof-level abstractions. One of the novelty of this logic is a new quantifier which actually gives rise to a different, generic, proof-level binder. We show that the new logic allows us to directly capture more distinctions of binding constructs in the encoded computational systems.
800 000 dans un corps fini
à 
éléments
Emmanuel Thomé
mercredi 27 novembre 2002, à 10H30
l
Les algorithmes sous-exponentiels de calcul d'index qui sont utilisés
pour résoudre des problèmes de logarithme discret passent toujours par
une phase d'algèbre linéaire. Nous avons récemment établi un record en la
matière, en calculant des logarithmes discrets dans
. À de nombreux égards, les proportions du calcul
furent gigantesques. Nous nous intéresserons plus particulièrement ici à
la phase d'algèbre linéaire, qui a nécessité la solution d'un système à
équations et inconnues, défini sur
, avec
. Fort heureusement,
ce système linéaire était un système ``creux'', puisque ``seulement''
millions de ses coefficients (soit 
) étaient non nuls. À la
connaissance de l'auteur, aucun système comparable n'a été résolu jusqu'à
présent.
La solution de ce système a nécessité la mise en oeuvre de moyens théoriques et pratiques très variés. Nous avons utilisé l'algorithme de Wiedemann par blocs, que nous avons amélioré. La structure de cet algorithme nous a permis de mener les calculs de manière décentralisée. Cet algorithme ne permet pas toutefois une totale parallélisation de l'algèbre linéaire, et il passe par une étape séquentielle. Nous esquisserons l'amélioration que nous avons apportée ici à l'algorithme, qui nous a permis d'effectuer ce pas séquentiel en 48 heures de calcul au lieu de trois mois, en utilisant des transformées de Fourier pour effectuer des produits de matrices de polynômes.
Nous donnerons des éléments de comparaison permettant de différencier les algorithmes d'algèbre linéaire creuse que sont les algorithmes de Wiedemann, Lanczos, leurs version ``par blocs'', l'élimination structurée, etc.
Nous donnerons aussi quelques détails et anecdotes sur l'histoire d'un calcul aux proportions si énormes, les volumes de données que cela a représenté (plusieurs dizaines de gigaoctets), les ordinateurs impliqués (plus de 150, sur plusieurs sites, dans l'ensemble du calcul de logarithme discret), la facilité ou la difficulté de l'accès aux ressources de calcul, et enfin l'épreuve intense que représente ces calculs pour le matériel.
l Many real world graphs, such as the WWW graphs, the internet graphs, co-actorship graphs, co-authorship graphs, protein graphs..., are known to be small world graphs. They are large in size but they have small average distance and high clustering coefficient (the connectivity between any two neighbors of a vertex). We noticed that many small world graphs are obtained by cliques additions. Based on this, we propose a realistic model by adding cliques with given distribution in size and overlapping ratio. We prove that the graphs generated by our model are small world graphs, the average distance is logarithmic with respect to the size of the graph and growing rate of the clustering coefficient is greater than 1/n, where n is the size of the graph. There are other models in the literature but only experimental proofs are given whereas we have theoretical proofs. This paper is a joint work with Matthieu Latapy and Jean-Loup Guillaume.
l La prediction de structure des macromolecules telles que les ARNs ou les proteines est un probleme majeur en biologie qui a donne naissance a de nombreux algorithmes et logiciels tentant d'y parvenir. Parmi ceux-ci, deux approches distinctes se degagent. La premiere consiste a chercher la structure minimisant une energie tandis que la seconde est regroupe les methodes comparative reposant sur une large base de donnees. Apres une presentation des methodes existantes nous nous interesserons a la prediction des structures d'ARNs par minimisation d'energie et modeliserons ce probleme a l'aide des grammaires S-attribuees. Ces dernieres constituent un formalisme souple permettant de developper une algorithmique efficace destinee a resoudre ces problemes. Afin d'illustrer ce propos, nous presenterons l'algorithme AMSAG et ses recentes applications.
l En 1990, J.F. Mestre propose un algorithme qui permet de retrouver une courbe hyperelliptique a partir de ses invariants. Malheureusement, cet algorithme ne s'applique que lorsque la caracteristique du corps de definition est differente de 2. Aujourd'hui, grace a des methodes p-adiques, on peut esperer resoudre ce probleme. Nous introduirons donc cet algorithme ainsi que les outils dont nous nous servirons. Cela nous conduira a parler des courbes hyperelliptiques et a definir leurs invariants. Puis nous evoquerons les nombres p-adiques. Enfin nous nous interesserons a la maniere de trouver un point sur une conique et a la maniere de revenir sur le corps de depart.
l Je commence par quelques rappels (difference entre crypto classique et crypto a cle publique, probleme du log discret, Diffie-Hellman, ElGamal, ) puis j'introduis les courbes elliptiques et les groupes associes (sans entrer dans les details). Je compte parler de la complexite du log discret (corps finis vs courbes elliptiques), puis j'attaque sur les couplages de Weil : proprietes, applications dans les attaques contre le log discret, puis applications dans les systemes bases sur l'identite, que je compte aussi definir au prealable. Enfin, je compte aussi aborder le probleme de la construction de courbes utilisables dans des systemes bases sur les couplages... et de conclure