Séminaire, 3 décembre 2015

Programme

10:30 – 12:00

Jonas Frey (Univ. Copenhagen (talk given in Salle des Thèses, ground floor))

Invited talk: Toposes from Krivine realizability with side effects

To start, I will give an introduction to the categorical approach to Krivine realizability, and in particular explain how Krivine realizability gives rise to toposes using Hyland, Johnstone and Pitts' "tripos-to-topos construction". Krivine realizability is parametric over the concept of "pole", and I will explain how to obtain new poles by augmenting the syntax with side effects for I/O. To conclude I will discuss potential links to algorithmic complexity theory, based on work in progress in collaboration with Jakob Grue Simonsen.

__This talk will be given in Salle des Thèses, ground floor__ (we will be in Amphi B in the afternoon).

14:00 – 15:00

Rodolphe Lepigre (Université de Savoie)

Invited talk: A call-by-value realizability model for PML

We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).

• slides

15:30 – 16:30

Yves Guiraud (INRIA)

Invited talk: Théorie de Squier et application aux monoïdes d'Artin

Un monoïde ayant une présentation par un système de réécriture convergent fini a un problème du mot décidable. Dans les années 1980, Jantzen s'interroge sur la réciproque : un monoïde de type fini ayant un problème du mot décidable admet-il toujours une présentation convergente finie ? Squier a répondu négativement à cette question en établissant une connexion entre des propriétés algorithmiques des systèmes de réécriture, comme la terminaison et la confluence, et des invariants algébriques, comme l'homologie ou l'homotopie.

Dans cet exposé, je présenterai le résultat initial de Squier, dans le formalisme contemporain de la réécriture de dimension supérieure. Puis je montrerai comment, avec Stéphane Gaussent et Philippe Malbos, nous avons adapté le théorème de Squier pour étudier des propriétés homotopiques des monoïdes de tresses et de leur généralisation, les monoïdes d'Artin.