2 décembre 2014

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

4 décembre 2014, 9:30 : Soutenance de thèse

Marc Bagnol (I2M), On the Resolution Semiring

Jury:

  • Pierre-Louis Curien
  • Jean-Yves Girard (directeur de thèse)
  • Ugo dal Lago (rapporteur)
  • Paul-André Melliès
  • Myriam Quatrini
  • Ulrich Schöpp
  • Philip Scott (rapporteur)
  • Kazushige Terui

We study in this thesis a semiring structure with a product based on the resolution rule of logic programming. This mathematical object was introduced initially in the setting of the geometry of interaction program in order to model the cut-elimination procedure of linear logic. It provides us with an algebraic and abstract setting, while being presented in a syntactic and concrete way, in which a theoretical study of computation can be carried on.

We will review first the interactive interpretation of proof theory within this semiring via the categorical axiomatization of the geometry of interaction approach. This interpretation establishes a way to translate functional programs into a very simple form of logic programs.

Secondly, complexity theory problematics will be considered: while the nilpotency problem in the semiring we study is undecidable in general, it will appear that certain restrictions allow for characterizations of (deterministic and non-deterministic) logarithmic space and (deterministic) polynomial time computation.

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), Some topics on hypersequents

5 décembre 2014, 10:30 : Soutenance de thèse

Michele Alberti (I2M/Focus), On operational properties of quantitative extensions of lambda-calculus

Jury:

  • Paul B. LEVY (University of Birmingham), Rapporteur
  • Simone MARTINI (Università di Bologna), Directeur
  • Michele PAGANI (Université Paris Diderot), Rapporteur
  • Laurent REGNIER (Aix-Marseille Université), Directeur
  • Simona RONCHI DELLA ROCCA (Università di Torino), Présidente

  • Emmanuel BEFFARA (Aix-Marseille Université), Directeur (invité)

  • Ugo DAL LAGO (Università di Bologna), Directeur (invité)
  • Lionel VAUX (Aix-Marseille Université), Directeur (invité)

Cette thèse porte sur les propriétés opérationnelles de deux extensions quantitatives du λ-calcul pur: le λ-calcul algébrique et le λ-calcul probabiliste. Dans la première partie, nous étudions la théorie de la β-réduction dans le λ-calcul algébrique. Ce calcul permet la formation de combinaisons linéaires finies de λ-termes. Bien que le système obtenu jouisse de la propriété de Church-Rosser, la relation de réduction devient triviale en présence de coefficients négatifs, ce qui la rend impropre à définir une notion de forme normale. Nous proposons une solution qui permet la définition d’une relation d’équivalence sur les termes, partielle mais cohérente. Nous introduisons une variante de la β-réduction, restreinte aux termes canoniques, dont nous montrons qu’elle caractérise en partie la notion de forme normale précédemment établie, démontrant au passage un théorème de factorisation.

Dans la seconde partie, nous étudions la bisimulation et l’équivalence contextuelle dans un λ-calcul muni d’un choix probabliste. Nous donnons une technique pour établir que la bisimilarité applicative probabiliste est une congruence. Bien que notre méthode soit adaptée de celle de Howe, certains points techniques sont assez différents, et s’appuient sur des propriétés non triviales de « désintrication » sur les ensembles de nombres réels. Nous démontrons finalement que, bien que la bisimilarité soit en général strictement plus fine que l’équivalence contextuelle, elles coïncident sur les λ-termes purs. L’égalité correspondante est celle induite par les arbres de Lévy-Longo, généralement considérés comme l’équivalence extensionnelle la plus fine pour les λ-termes en évaluation paresseuse.

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.