23 avril 2015, 11:00 : Séminaire

Pierre Hyvernat (LAMA, université de Savoie), Représentation des fonctions continues entre « streams » (& Co.) par des types de données

Brouwer savait déjà que les fonctions continues entre streams (avec la topologie produit habituelle) pouvaient être représentées par des arbres infinis. Peter Hancock a montré comment interpréter ce théorème de représentation en théorie des types dépendants, permettant ainsi de manipuler ces fonctions comme un type de données (co)inductif standard.

Nous avons récemment pu généraliser ces idées à de nombreux types de données coinductifs en utilisant la notion de structure d'interaction (ou « container indexé » ou « foncteur polynomial »). Je présenterai cette généralisation en essayant d'introduire les notions nécessaires au fur et à mesure : topologie produit, types dépendants, définitions inductives et coinductives, systèmes d'interaction, définitions inductive-récursives, etc.

(Travail avec Peter Hancock)

21 mai 2015

Séminaire Chocola à Lyon.

Du 8 au 12 juin 2015

Rencontre du GT GéoCal du GDR-IM (voir le programme).

18 juin 2015, 11:00 : Séminaire

Fabio Zanasi (LIP, ÉNS Lyon), Interacting Hopf algebras: the string diagrammatic theory of linear subspaces

We introduce the theory IH of interacting Hopf algebras, parametrised over a principal ideal domain R. The axioms of IH are derived using Lack’s approach to composing PROPs: they feature two Hopf algebras and two Frobenius algebras. This construction is instrumental in showing that IH is a presentation by generators and equations of the PROP of linear relations (i.e. subspaces) over the field of fractions of R.

The equational theory IH turns out to be useful in various contexts. For R=Z, it expresses rational subspaces. The case R=Z_2 is of importance for describing quantum computation. In this talk we will focus on the case R=k[x], in which IH yields a compositional stream semantics for linear dynamical systems (signal flow graphs).