27 novembre 2014, 11:00 : Séminaire

Thomas Seiller (IHÉS), Des invariants de cohomologie pour la complexité?

J'exposerai des résultats récents à l'intersection entre mes travaux sur les graphes d'interaction et ceux concernant la complexité.

Mon travail sur les graphes d'interaction m'a mené à une construction systématique de modèles de la logique linéaire basée sur la notion de « graphage » — des réalisations de graphes par des fonctions mesurables. Intuitivement, un graphage est un graphe dont les sommets sont des ensembles mesurables et les arêtes sont « réalisées » par des fonctions mesurables. Ces modèles sont caractérisés par un monoide de fonctions (mesurables) qui décrit les différents manières de réaliser une arête.

Je montrerai que le choix de ce monoide correspond à imposer des contraintes de complexité. Cette correspondance est illustrée par l'obtention de modèles de MALL avec des exponentielles (très) faibles où le type des prédicats sur les entiers binaires !Nat_2 ⊸ Bool caractérise des classes de complexité telles que les languages réguliers, L (logspace), NL, Ptime.

Ces résultats permettent d'envisager l'utilisation d'invariants de cohomologie pour étudier les classes de complexité.

2 décembre 2014

Journée Logique à Marseille organisée par Nicolas Olivetti et Luigi Santocanale.

4 décembre 2014 : Chocola à Marseille

Séminaire Chocola à Marseille, avec les soutenances de Marc Bagnol (le 4 décembre) et Michele Alberti (le 5 décembre).

11:00: Paul Blain Levy (Birmingham), Transition systems over games
14:00: Guillaume Geoffroy (ÉNS), (à préciser)
15:30: Kazushige Terui (RIMS, Tokyo), (à préciser)

11 décembre 2014, 14:00 : Séminaire

Guillaume Brunerie (Nice), Théorie des types cubique

Je présenterai des travaux en cours (en collaboration avec Dan Licata) sur le développement d’une théorie des types cubique, le but étant d’obtenir une théorie des types ayant de bonnes propriétés calculatoires (normalisation forte, canonicité, décidabilité du typage) tout en étant compatible avec la théorie des types homotopiques, en particulier avec l’axiome d’univalence et les types inductifs supérieurs. Ces travaux sont égalements très liés aux travaux de Thierry Coquand, Simon Huber et Marc Bézem sur un modèle constructif de la théorie des types homotopiques dans les ensembles cubiques.