Séminaires du LAMA

Séminaires hebdomadaires (Salle TLR, voir Comment venir).

Autres séminaires :

Prochains séminaires du LAMA :

EDPs²Vendredi 03 mai 2019 à 14h Friedemann Brock (University Swansea),
Isoperimetric inequalities w.r.t. homogeneous weights and symmetry of optimal functions in CKN inequalities

GéométrieJeudi 23 mai 2019 à 14h 80 ans du CNRS (LAMA),
à venir

Résumé : (Masquer les résumés)
à venir

LIMDJeudi 25 avril 2019 à 10h Peio Borthelle (LAMA),
Ornements & induction-récursion

Résumé : (Masquer les résumés)
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.