Parmi les nombreuses structures ordonnées liées aux espaces topologiques, les treillis continus occupent une place importante. Ils constituent par exemple les espaces topologiques de Kolmogorov injectifs. Nous nous proposons ici de présenter ces treillis d'un point de vue algébrique au travers de la notion de monade et d'adjonction de Galois. La définition originelle d'espace topologique donnée par Hausdorff en 1914 apparaît alors de façon naturelle, et nous permet de jeter un regard neuf sur le résultat d'injectivité mentionné ci-dessus.
Voir la page dédiée.
TBA
Nous construisons une structure de modeles de Quillen pour la categorie des omega-categories strictes, a partir d'un ensemble de cofibrations generatrices et d'une classe d'equivalences faibles. Toute omega-categorie est fibrante par rapport a cette structure, alors que les omega-categories cofibrantes sont precisement les libres.
Cet exposé est divisé en deux parties distinctes présentant deux sujets de recherche autour de la Logique Linéaire. Bien qu'abordés il y a longtemps, ces sujets présentent toujours des questions ouvertes intéressantes. L'exposé pose plus de questions qu'il ne donne de réponses.
Le premier sujet concerne la notion de structure en Logique Linéaire. De nombreuses extensions de la Logique Linéaires ont été proposées dans le passé pour introduire une forme de structure qui dépasse celle de multi-ensemble: logique cyclique, logique non commutative, calcul de Lambek non associatif (qui en fait prédate la Logique Linéaire)... Un cadre général, appelé ``Logiques Linéaires Colorées'', a été proposé pour capturer les mécanismes communs à toutes ces extensions, et permettant d'en construire d'autres à l'infini, respectant automatiquement les propriétés essentielles d'élimination de la Coupure et de focalisation (ce travail montre d'ailleurs que ces deux propriétés sont intimement liées). La question ouverte est de comprendre quels critères supplémentaires permettent de séparer, dans cette infinité potentielle de systèmes, le bon grain de l'ivraie, avec l'idée sous-jacente que la Logique devrait avoir un caractère de nécessité, et ne pas laisser place à l'arbitraire.
Le deuxième sujet concerne un paradigme de programmation fondé non pas sur la réduction des coupures dans les réseaux de preuves mais sur la construction de réseaux de preuves en Logique Linéaire. La construction de réseaux, comme la réduction, peut se faire en parallèle, mais, contrairement à la réduction, il y a des séquentialisations irréductibles, qu'exprime la nécessité de respecter le critère de correction. Le paradigme résultant est très proche de celui, plus pragmatique, des systèmes transactionnels, issus du monde des bases de données, mais dont les mécanismes sont aujourd'hui présents dans les couches intergicielles de toutes les grandes applications réparties. Un mécanisme de construction incrémental de réseaux de preuves a été proposé dans le passé dans le cadre du fragment strictement multiplicatif de la Logique Linéaire. Les questions ouvertes sont ici de savoir si ce mécanisme est optimal pour le fragment visé d'une part et d'autre part s'il peut être étendu à des fragments plus larges, voire au système complet.
Deuxième séance du groupe de lecture sur le livre de Kohlenbach ``Applied Proof Theory''.
Developing effective reasoning techniques for languages with higher- order constructs is a challenging problem, made even more challenging with the presence of concurrency and mobility. In this talk I will present a practical and effective reasoning methodology for such a language, which employs first-order reasoning and handles examples in a straightforward manner. There are two significant aspects to this theory. The first is that higher-order inputs are treated in a first- order manner, hence eliminating the need to reason about arbitrarily complicated higher-order contexts, or to use up-to context techniques, when establishing equivalences between processes. The second is that we use augmented processes to record directly the knowledge of the observer. This has the benefit of making ordinary first-order weak bisimulation fully abstract w.r.t. contextual equivalence. It also simplifies the handling of names, giving rise to a truly propositional Hennessy-Milner characterisation of higher-order contextual equivalence. I will illustrate the simplicity of the approach with example equivalences and inequivalences, and use it to show that contextual equivalence in a higher-order setting is a conservative extension of the first-order pi-calculus.
La séance précédente était consacrée aux algèbres de Boole et aux notions de filtre, d'idéal et d'ultrafiltre. Cette séance sera consacrée à la définition de la notion de modèle Booléen (en insistant sur les problèmes soulevés par cette définition) et à l'étude de ses propriétés: validité, complétude, etc. Je présenterai les principales constructions attachées aux modèles booléens: produit, quotient, ultraproduit, ultrapuissance. Je terminerai en montrant comment la théorie peut être appliquée à la construction des modèles de l'analyse non standard.
Voir la page dédiée.
En combinatoire des mots et plus précisément dans l'étude des mots unidimensionnels, la notion de mot de retour a joué un rôle important, en particulier dans la caractérisation des mots sturmiens. Ces mots servant de représentation pour les droites discrètes, il est tout naturel de se poser la question d'une caractérisation en dimension supérieure, en particulier dans le cas des plans discrets. En dimension 2, on vient à considérer des mots bidimensionnels. Les notions habituelles doivent donc être adaptées. Nous verrons que le passage à la dimension 2 provoque de vrais problèmes vis à vis de définitions simples en dimension 1.
Je présente un lambda calcul codant une logique intuitionniste du second ordre et permettant de programmer un ou-parallèle''. Ce calcul a les propriétés suivantes :préservation de type'', forte normalisation'' etunicité de représentation des données''. Il permet aussi d'écrire des programmes avec une sorte d'exception. Il est inspire du lambda-mu-{++}-calcul que j'ai introduit en 2002.
En 1962, Cohen a résolu le premier problème de Hilbert en montrant que l'hypothèse du continu est indécidable dans la théorie des ensembles de Zermelo-Fraenkel. La technique qu'il a introduite pour établir ce résultat non trivial - le forcing - est devenue aujourd'hui un outil standard en théorie des modèles. Cette technique a permis d'établir de nombreux autres résultats de cohérence relative (ou d'indépendance), comme par exemple la cohérence de l'axiome de Solovay: « toute partie de R est mesurable au sens de Lebesgue » dans une théorie des ensembles sans axiome du choix (mais avec choix dépendant).
Dans cet exposé introductif au forcing, je me propose de présenter la théorie des modèles booléens, une variante du forcing (introduite par Scott, Solovay et Vopenska dans les années 1960) qui permet de faire essentiellement les mêmes constructions que Cohen, mais dans un cadre qui est plus facile à saisir au premier abord. J'introduirai les notions de base (algèbres de Boole, ultrafiltres, modèles booléens, quotient, produit, ultraproduit et ultrapuissance) tout en illustrant mon propos par quelques exemples de constructions, notamment en lien avec l'« analyse non standard ».
La preuve de l'indépendance de l'hypothèse du continu à l'aide de ces outils fera l'objet de l'exposé suivant.
In 2003, Hofmann and Jost introduced a type system that uses a potential-based amortized analysis to infer bounds on the resource consumption of (first-order) functional programs. This analysis has been successfully applied to many standard algorithms but is limited to bounds that are linear in the length of the input.
Here we extend this system to polynomial resource bounds. An automatic amortized analysis is used to infer these bounds for functional programs without further annotations if a maximal degree for the bounding polynomials is given. The analysis is generic in the resource and can obtain good bounds on heap-space, stack-space and time usage. Furthermore, the analysis can be used to infer polynomial relations between the input and the output sizes of a function in the sense of sized types.
Travail en collaboration avec Jan Hoffmann.
The wire calculus is a process algebra for modelling truly concurrent systems with explicit network topologies. It benefits from using categorical operators for coordination of processes: the tensor product and sequential composition of monoidal categories. The dynamics are handled by operators inspired by Milner's CCS and Hoare's CSP: unary prefix operation, binary choice and a standard recursion construct. The operational semantics is a labelled transition systems derived using SOS rules. After presenting the formal definition of the calculus I will discuss some basic results and give several examples.
Les différentes parties de mes travaux de thèse en géométrie discrète et géométrie algorithmique seront présentées durant cet exposé.
Partie 1 : Nous considérons tout d’abord le problème de l’approximation d’un nombre réel par un nombre rationnel de dénominateur borné. Soit a un nombre réel, soit b et b’ deux nombres entiers tels que b<b’, nous souhaitons déterminer le nombre rationnel r=p/q qui approxime au mieux a, tel que b <= q <= b’. La principale approche numérique connue utilise le développement en fraction continue du réel a. Géométriquement, ce problème revient à déterminer le point de la grille le plus proche de la droite d’équation y=ax compris dans un domaine vertical défini par {(x,y) | b <= x <= b’}. Nous proposons de calculer l’enveloppe convexe des points de la grille situés au dessus (resp. en dessous) de la droite et compris dans le domaine vertical. Notre algorithme atteint une complexité logarithmique en la largeur du domaine vertical. De plus, il est adaptatif puisque le nombre d’itérations en temps constant effectuées par notre algorithme est exactement égal au nombre de sommets des deux enveloppes convexes calculées.
Partie 2 : Par la suite, nous présenterons notre algorithme de reconnaissance de plans discrets. Nous rappelons qu’un ensemble de points S de Z^3 est appelé morceau de plan discret s’il est contenu dans la discrétisation d’un plan euclidien. Un tel algorithme est utilisé pour décider si un sous-ensemble de points d’un objet discret peut être remplacé par une facette dans une représentation polyédrique de l’objet. La méthode proposée décide si un sous-ensemble de points de Z^3 correspond à un morceau de plan discret en résolvant un problème de réalisabilité sur une fonction convexe en dimension 2, dite fonction épaisseur. Ainsi, notre méthode ne prend en compte que deux paramètres et elle utilise des techniques géométriques planaires pour déterminer si l’espace des solutions est vide. Notre algorithme s’exécute en O(n log D) dans le pire cas ou n correspond au nombre de points de l’ensemble S et D représente la taille d’une boite englobant S. Notre méthode s’avère également efficace en pratique et reconnaît un ensemble de 10^6 points en environ 10 itérations linéaires.
Partie 3 : Si le temps nous le permet, nous aborderons enfin une problématique un peu à part : calculer l’épaisseur d’un ensemble de points de Z^d dans le réseau entier de même dimension (épaisseur latticielle). L’épaisseur d’un ensemble de points K suivant une direction c de Z^d correspond à la quantité max{c.x | x \in K} - min{c.x | x \in K}. L’épaisseur latticielle de l’ensemble de points K correspond à l’épaisseur minimum pour toutes les directions du réseau. D’après une idée originale de Fabien FESCHET, nous avons mis en place un algorithme valable en toute dimension pour déterminer cette épaisseur. Cette méthode s’avère optimale puisque linéaire en temps dans le cas planaire. En dimensions supérieures, nous passons par une approche gloutonne qui s’avère efficace en pratique.
TBA
L'exposé sera pour un public de non spécialistes. J'essaierai de raconter ce qu'est un bon langage de programmation (selon moi) et donc ce qu'est PML. J'essaierai notamment d'expliquer les points suivants:
Je ferai un premier exposé de complexité de communication, et un deuxième sur nos résultats sur les applications entre cette théorie et les automates cellulaires. Il y aura un peu de machines de Turing, pas mal d'automates cellulaires, beaucoup de complexité de communication, et aussi des circuits logiques. La complexité de communication est une théorie très générale, et il y a plein d'applications en complexité (parallèle et séquentielle), mais aussi des choses plus appliquées comme le design de processeurs, des problèmes de graphes, etc. En plus, c'est un modèle de calcul qui n'a pas besoin de la thèse de Church.
Dans cet exposé, je présenterai une famille de polyominos appelés doubles carrés, ayant la propriété de paver le plan par translation de deux façons distinctes. Rappelons qu'un polyomino est un sous-ensemble de la grille discrète qui est 4-connexe (connecté verticalement et horizontalement) et sans trou (c'est-à-dire que son complément est également 4-connexe). Nous pouvons en particulier coder son contour par un mot sur un alphabet à quatre lettres {h, b, g, d} codant les déplacements 'haut', 'bas', 'gauche' et 'droite'. J'introduirai d'abord les définitions de la combinatoire des mots nécessaires à cet exposé ainsi que les notions de polyominos et de pavages. Ensuite, je survolerai rapidement les résultats connus et certaines conjectures intéressantes. J'enchaînerai en présentant quelques propriétés sur les chemins liées à une généralisation de la notion de palindrome et je terminerai en présentant une famille de tuiles liées à la suite de Fibonacci. L'exposé se déroulera en québécois...
Des entreprises comme Amazon, Google et Yahoo rendent maintenant disponibles une partie de leurs fonctionnalités sous la forme de services web; une application tierce peut communiquer avec ces services via Internet en échangeant des messages dont la structure et le contenu sont publics et formellement définis. Cependant, la documentation précise également une foule d'autres détails sur la manière dont ces services doivent être consommés, exprimés en langue naturelle et échappant à toute formalisation. Ce contexte nous a amené à développer LTL-FO+, une extension de la logique temporelle LTL incluant 1) une forme particulière de quantification du premier ordre; 2) une sémantique à 2, 3 ou 4 valeurs de vérité, selon le contexte. On verra que, contrairement à LTL, elle est appropriée pour exprimer des contraintes sur les séquences de messages propres aux applications web. On s'intéressera par la suite à son runtime monitoring; pour ce faire, nous présenterons BeepBeep, un outil permettant la vérification et l'application de formules LTL-FO+ en temps réel sur de vraies applications web. Finalement, on verra au moyen d'un exemple concret (si la connexion Internet le permet) comment BeepBeep: 1) empêche une application web mal programmée de commettre des erreurs; et 2) nous permet de découvrir que les services web d'Amazon ne respectent pas certains détails de leur propre documentation.