Seminars of LAMA

Four regular seminars take place at LAMA, in the seminar room, first floor of the building Le Chablais, (see How to come ?).

Weekly seminars:

Others seminars

Next seminars:

EDPs²Friday 3rd May 2019 at 14h Friedemann Brock (University Swansea),
Isoperimetric inequalities w.r.t. homogeneous weights and symmetry of optimal functions in CKN inequalities

GéométrieThursday 23rd May 2019 at 14h 80 ans du CNRS (LAMA),
à venir

Abstract: (Hide abstracts)
à venir

LIMDThursday 25th April 2019 at 10h Peio Borthelle (LAMA),
Ornements & induction-récursion

Abstract: (Hide abstracts)
Les types dépendants permettent de rajouter des preuves d'invariants dans les structures de données et ainsi de faire des programmes corrects par construction. L'envers de la médaille est une multiplication des structures subtilement différentes pour lesquelles il faut prouver des lemmes similaires de manière répétée. L'ornementation est un outil méta-théorique introduit par Conor McBride qui permet de décrire ces relations et apporte avec lui une boite à outils de méta-programmation. J'ai étendu cette notion aux types inductifs-récursifs, des définitions simultanées d'une structure et d'un éliminateur. Ceux-ci sont nécessaires pour définir certains gros univers mais apparaissent également ``dans la vie courante''. Je m'attarderai surtout sur des exemples et leur axiomatisation méta- théorique qui a récemment progressée.