Le séminaire de l’équipe LIMD est sous la responsabilité de Xavier Provençal.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2013, 2014, 2015, 2016, 2017, toutes ensemble.

Année 2012

Jeudi 20 décembre 2012 à 10h Clément Fumex (University of Strathclyde),
Schémas d'induction et de coinduction dans les fibrations

Résumé : (Masquer les résumés)
En théorie des catégories, une fibration représente une forme d'indexation d'une catégorie par une autre. On rappellera comment une telle structure peut être utilisée pour modéliser une logique (représentée par la catégorie indexée) au dessus d'une théorie des types (représentée par la catégorie index). On portera alors notre attention sur les types inductifs et coinductifs et comment capturer leurs schémas d'induction et de coinduction respectif dans les fibrations.

Jeudi 13 décembre 2012 à 10h Damien Pous (LIP, ENS Lyon),
Checking NFA equivalence with bisimulations up to congruence

Résumé : (Masquer les résumés)
We introduce ``bisimulation up to congruence'' as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weaker ``bisimulation up to equivalence'' technique. The resulting algorithm can be exponentially faster than the recently introduced ``antichain algorithms''.

Jeudi 29 novembre 2012 à 10h Marc Bagnol (IML),
Les machines synchrones: une catégorie à trace

Résumé : (Masquer les résumés)
Les catégories à trace ont été utilisées dans le domaine de la sémantique dénotationnelle (en logique comme en informatique) pour modéliser des situations de rétroaction ``raisonnables''. La construction G(.) permet, à partir d'une catégorie à trace, d'obtenir une nouvelle catégorie dont la composition peut être vue comme une ``rétroaction parallèle''. Les ``machines synchrones'' ont été utilisées pour donner une sémantique des langages de programmation synchrones (Lustre, Esterel...) en termes d'automates. Dans ces sémantiques, la mise en parallèle de deux programmes est modélisée par une construction appelée ``produit synchrone''. On verra que les machines synchrones peuvent être vues comme une catégorie à trace S et que le produit synchrone de deux machines correspond à leur composition dans G(S).

Jeudi 22 novembre 2012 à 10h Jean-Marie Madiot (LIP, ENS Lyon),
Sous-typage en pi-calculs

Résumé : (Masquer les résumés)
Le système de types input/output induit du sous-typage dans le pi-calcul. De manière un peu surprenante, le sous-typage se prête mal à une adaptation à des calculs proches (le calcul des fusions, le pi-calcul à mobilité interne). On construit une modification du calcul des fusions dans laquelle le mécanisme du sous-typage s'applique, ce qui permet d'en éclairer certains aspects.

Jeudi 25 octobre 2012 à 10h Pierre Clairambault (Cambridge),
The biequivalence of locally cartesian closed categories and Martin-Löf type theories

Résumé : (Masquer les résumés)
Seely’s paper Locally cartesian closed categories and type theory contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Löf type theories with Π, Σ, and extensional identity types. However, Seely’s proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely’s theorem: that the Bénabou-Hofmann interpretation of Martin-Löf type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-Löf type theories. As a second result we prove that if we remove Π-types the resulting categories with families are biequivalent to left exact categories.

Jeudi 18 octobre 2012 à 10h Damiano Mazza (LIPN, Université Paris Nord),
Non-Linearity as the Metric Completion of Linearity

Résumé : (Masquer les résumés)
It is well known that the real numbers arise from the metric completion of the rational numbers, with the metric induced by the usual absolute value. We seek a computational version of this phenomenon, with the idea that the role of the rationals should be played by the affine lambda-calculus, whose dynamics is finitary; the full lambda-calculus should then appear as a suitable metric completion of the affine lambda-calculus. We propose a technical realization of this idea: we introduce an affine lambda-calculus, based on a fragment of intuitionistic multiplicative linear logic; the calculus is endowed with a notion of distance making the set of terms an incomplete metric space; we show that the completion of this space yields an infinitary affine lambda-calculus, whose quotient under a suitable partial equivalence relation is exactly the full (non-affine) lambda-calculus. We also show how this construction brings interesting insights on some standard rewriting properties of the lambda-calculus (finite developments, confluence, standardization, head normalization and solvability).

Mardi 09 octobre 2012 à 14h Romain Demangeon (Queen Mary, University of London),
Verification of Protocols with Session Types

Résumé : (Masquer les résumés)
Introduced as symmetric types for pi-processes, session types have been developed into a large theory for verification of message-passing programs. Their main principle is as follows: a global type describing the expected interactions inside a network is projected into several local types: if every agent abides to its local type, the whole network abides to the global specification. I will present the Multiparty Session Types theory through recent developments: full-abstract embedding into the pi-calculus, nested protocols, automatic monitor generation, session types with multisession assertions.

Jeudi 27 septembre 2012 à 10h Christophe Raffalli (LAMA, LIMD),
Réalisabilité, Ramsey et ultrafiltre

Résumé : (Masquer les résumés)
On regardera les programmes que l'on peut extraire des preuves du théorème de Ramsey infini. On ira jusqu'à extraire un programme SML pour le ``happy ending problem'', qui trouve P sommets d'un polyogone convexe à partir de N points du plan si N est assez grand (http://fr.wikipedia.org/wiki/Happy_Ending_problem). On regardera aussi le programme que donne la preuve de Ramsey par l'ultrafiltre par rapport à la preuve classique. Enfin, on se posera des questions sur les liens possibles entre la compléxité des programmes liés à Ramsey et des bornes sur la fonction de Ramsey.

Jeudi 12 juillet 2012 à 14h30, Amphi Nivolet Ivan Rapaport (CMM, Universidad de Chile),
Short messages and local knowledge in distributed systems

Résumé : (Masquer les résumés)
We study distributed algorithms on massive graphs where links represent a particular relationship between nodes (for instance, nodes may represent phone numbers and links may indicate telephone calls). Since such graphs are massive they need to be processed in a distributed and streaming way. When computing graph-theoretic properties, nodes become natural units for distributed compu- tation. Links do not necessarily represent communication channels between the computing units and therefore do not restrict the communication flow. Our goal is to model and analyze the computational power of such distributed systems where one computing unit is assigned to each node.

Jeudi 21 juin 2012 à 11h, Salle réunion Mont-Blanc Colin Riba (LIP, ENS Lyon),
A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Streams

Résumé : (Masquer les résumés)
We discuss a complete axiomatization of Monadic Second-Order Logic (MSO) on infinite words (or streams). By using model-theoretic methods, we give an alternative proof of D. Siefkes’ result that a fragment with full comprehension and induction of second-order Peano’s arithmetic is complete w.r.t. the validity of MSO-formulas on streams. We rely on Feferman-Vaught Theorems and the Ehrenfeucht-Fraisse method for Henkin models of MSO. Our main technical contribution is an infinitary Feferman-Vaught Fusion of such models. We show it using Ramseyan factorizations similar to those for standard infinite words.

Jeudi 14 juin 2012 à 10h Anna Frid (Sobolev Institute of Mathematics),
Comptage des mots engendrés par intervalles

Résumé : (Masquer les résumés)
Nous considérons la famille des problèmes reliés au comptage des mots sur un alphabet fini engendrés par intervalles, y compris les mots sturmiens, des mots de rotation et les mots engendrés par l'échange de trois intervalles. Nous discutons des méthodes géométriques et combinatoires de comptage.

Jeudi 31 mai 2012 à 10h Srecko Brlek (LaCIM, Université du Québec à Montréal),
Quelques remarques sur les trajectoires exponentielles d'Oldenburger

Résumé : (Masquer les résumés)
Hedlund et Morse ont introduit et développé la dynamique symbolique vers 1938. La combinatoire des mots leur doit beaucoup, car ils ont mis en évidence de nombreux concepts important mais semblent avoir ignoré les trajectoires exponentielles de Rufus Oldenburger...

Jeudi 24 mai 2012 à 10h Pawel Sobocinski (University of Southampton, UK),
Combinators for Petri Nets with boundaries

Résumé : (Masquer les résumés)
I will talk about two novel models of Petri nets with boundaries and characterise them using a calculus of combinators.

Mercredi 16 mai 2012 à 10h15, Salle réunion Mont-Blanc Simon Perdrix (LIG, CAPP),
Completeness of algebraic CPS simulations

Résumé : (Masquer les résumés)
The algebraic lambda calculus and the linear algebraic lambda calculus are two extensions of the classical lambda calculus with linear combinations of terms. They arise independently in distinct contexts: the former is a fragment of the differential lambda calculus, the latter is a candidate lambda calculus for quantum computation. Their operational semantics differ in the treatment of applications and algebraic rules. We show how these two languages can simulate each other using an algebraic extension of the well-known call-by-value and call-by-name CPS translations. We prove that the simulations are sound and complete. Joint work with Ali Assaf, Alejandro Díaz-Caro, Christine Tasson and Benoît Valiron.

Jeudi 03 mai 2012 à 10h Samer Allouch (LAMA, LIMD),
Classification des catégories finies

Résumé : (Masquer les résumés)
On étudie dans cette thèse la relation entre les catégories finies et les matrices carrées positives, ensuite on arrive à étudier l'état de l'ensemble Cat(M) : s'il est vide ou non et déterminer ses bornes si c'est possible.

Jeudi 26 avril 2012 à 10h Tom Hirschowitz (LAMA, LIMD),
Une sémantique de jeux pour CCS (SUITE)

Résumé : (Masquer les résumés)
(suite de l'exposé précédent) On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.

Dimanche 01 avril 2012 à 10h Karim Nour (LAMA, LIMD),
Les contres exemples d'Andrew Polonski

Résumé : (Masquer les résumés)
(disponible prochainement)

Jeudi 29 mars 2012 à 10h Pascal Vanier (LIF, Marseille),
Degrés Turing des pavages

Résumé : (Masquer les résumés)
Dans cet exposé, on étudie les ensembles de degrés Turing associés aux pavages générés par un jeu de tuile. En particulier, on prouve qu'il existe un quasi-isomorphisme entre n'importe quelle classe Pi01 de {0,1}^N et un pavage. Pour cela, on introduit une construction permettant d'avoir du calcul tout en ayant un nombre dénombrable de pavages.

Jeudi 08 mars 2012 à 10h Tom Hirschowitz (LAMA, LIMD),
Une sémantique de jeux pour CCS

Résumé : (Masquer les résumés)
On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.

Jeudi 19 janvier 2012 à 10h Etienne Duchesne (LIPN - Paris-Nord),
MELL in a free compact closure

Résumé : (Masquer les résumés)
The categorical presentation of the standard model of the geometry of interaction –namely the free compact closure of sets and partial injections Int(PInj)– fails to be a denotational semantics of MELL. The work of Melliès, Tabareau & Tasson on the formula for a free exponential modality gives us insights into the reasons of this failure: absence of free pointed objects, absence of equalizers of some groups of permutations... We will present generic constructions which successively add the algebraic structure needed to compute this formula, and show that the usual model of GoI wrapped in these successive layers defines a denotational semantics of MELL.

Jeudi 05 janvier 2012 à 10h Assia Mahboubi (LIX),
Vers une vérification formelle de la preuve du théorème de Feit-Thompson

Résumé : (Masquer les résumés)
Le théorème de Feit-Thompson (1963) est un résultat historique de théorie des groupes finis. En effet, il permet de comprendre la structure de tous les groupes finis simples d'ordre impair et constitue ainsi une étape importante dans la classification des groupes finis simples qui est considérée comme achevée depuis les années 80. Néanmoins cette classification a un statut controversé car elle résulte de la compilation d'un nombre considérable de publications hétérogènes et parfois encore mal comprises. La preuve du théorème de Feit-Thompson est elle-même imposante, par sa taille et par la variété des résultats sur lesquels elle repose (théorie des groupes, algèbre linéaire, théorie de Galois, caractères,...). Elle est un défi pour les assistants à la preuves, logiciels permettant de représenter énoncés et preuves mathématiques sous la forme de termes logiques, vérifiables mécaniquement par un ordinateur. Dans cet exposé, qui ne présuppose aucune connaissance préalable en théorie des groupes, nous essaierons de montrer quels problèmes sont posés par une telle formalisation, par la représentation des objets mathématiques mis en jeu en théorie des types et en particuliers les solutions qui ont été trouvées pour faire vérifier (une partie conséquente de) cette preuve par l'assistant à la preuve Coq.

Le séminaire de l’équipe LIMD est sous la responsabilité de Xavier Provençal.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2013, 2014, 2015, 2016, 2017, toutes ensemble.