Les séminaires sont communs avec l'équipe Plume (ENS Lyon) et ont lieu en salle de séminaire, premier étage du bâtiment Le Chablais, sur le site du Bourget du Lac ou à l'ENS Lyon.

Prochain séminaire :

Jeudi 06 juin 2019 à 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Le séminaire de l’équipe LIMD est sous la responsabilité de Sebastien Tavenas.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, toutes ensemble.

Année 2019

Jeudi 20 juin 2019 à 10h Guillaume Geoffroy (Institut de mathématiques de Marseille),
TBA

Résumé : (Masquer les résumés)
TBA

Jeudi 13 juin 2019 à 10h Florent Capelli (Université de Lille),
TBA

Mercredi 12 juin 2019 à 10h Dr. Hassen KTHIRI (University of Sfax - Department of Mathematics),
TBA

Résumé : (Masquer les résumés)
TBA

Jeudi 06 juin 2019 à 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Jeudi 16 mai 2019 à 10h Sergueï Lenglet (Université de Lorraine),
Diacritical Companions

Résumé : (Masquer les résumés)
This talk will explain the each word in the title separately, and then how they can be combined together. Our problem is how to make coinductive equivalence proofs easier, and in particular how to prove sound enhancements of the bisimulation proof technique (also called up-to techniques). The lingua franca of this talk will be the lambda-calculus.

Jeudi 09 mai 2019 à 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Jeudi 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.

Jeudi 11 avril 2019 à 10h Rodolphe Lepigre (Max Planck Institute, Sarrebruck),
Une introduction rapide à la logique de séparation concurrente Iris

Résumé : (Masquer les résumés)
La logique de séparation concurrente est un formalisme qui permet de raisonner sur des programmes impératifs (manipulant des pointeurs) et concurrents. Dans cet exposé, je vous donnerai un aperçu des principes généraux sur lesquels est basé le système Iris, développé par Derek Dreyer et ses collaborateurs.

Jeudi 04 avril 2019 à 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Jeudi 28 mars 2019 à 10h Valentin Blot (Laboratoire Spécification et Vérification (École normale supérieure Paris-Saclay)),
TBA

Résumé : (Masquer les résumés)
TBA

Jeudi 21 mars 2019 à 10h Daniel Martins-Antunes (LAMA),
Digital Curvature Evolution Model for Image Segmentation

Résumé : (Masquer les résumés)
Recent works have indicated the potential of using curvature as a regularizer in image segmentation, in particular for the class of thin and elongated objects. These are ubiquitous in biomedical imaging (e.g. vascular networks), in which length regularization can sometime perform badly, as well as in texture identification. However, curvature is a second-order differential measure, and so its estimators are sensitive to noise. State-of-art techniques make use of a coarse approximation of curvature that limits practical applications. In this talk I propose the use of multigrid convergent estimators instead, and I will show a new digital curvature flow derived from it that mimics continuous curvature flow. Finally, an application as a post-processing step to a variational segmentation framework is presented.

Jeudi 14 mars 2019 à 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Jeudi 14 mars 2019 à 10h Guillaume Malod (IMJ-PRJ (Paris 7)),
Séries formelles et calculs non-commutatifs

Résumé : (Masquer les résumés)
Cet exposé s'inspire de la connexion remarquée récemment entre les séries formelles et calculs non-commutatifs et qui permet de retrouver très simplements des résultats de Nisan et d'autres sur les calculs non-commutatifs de polynômes. Je présenterai les résultats de base sous l'angle des séries formelles puis je montrerai l'application aux calculs monotones (commutatifs) et les perspectives et difficultés pour utiliser ces techniques pour des modèles avec moins de restrictions.

Jeudi 07 février 2019 à 10h Adrien Durier (LIP, ENS Lyon),
Fonctions et processus concurrents

Résumé : (Masquer les résumés)
La sémantique d'un programme est souvent donnée d'une des deux façons suivantes: ou bien comme une fonction mathématique (la fonction qu'il calcule) ou bien par le biais de son execution. La première méthode tend à détruire toute information fine sur le programme (complexité par exemple), alors que la seconde impose un cadre de bas niveau, syntaxique, sans la structure et les propriétés mathématiques donnés par la première. Pour allier les avantages des deux méthodes, de nombreux sémanticiens s'intéressent à représenter les programmes comme des interactions (interactions qui se déroulent entre un programme et son contexte); ceci en permet une compréhension dynamique. Le lambda-calcul est un formalisme standard pour représenter les programmes fonctionnels. Le pi-calcul, lui, fournit un outil pour représenter leurs interactions. Milner a montré en 1990 comment interpréter le lambda-calcul dans le pi-calcul. Plus précisément, il a montré comment interpréter deux stratégies d'évaluations du lambda-calcul, l'appel par nom et l'appel par valeurs. Se pose alors le problème de Full Abstraction: pour quelle notion d'équivalence de programme ces interprétations sont-elles correctes et complètes ? Si le problème a été résolu rapidement pour l'appel par nom, l'appel par valeur pose davantage de problèmes techniques...

Jeudi 24 janvier 2019 à 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Le séminaire de l’équipe LIMD est sous la responsabilité de Sebastien Tavenas.
Options : Voir par date croissante . Masquer les résumés.
Autres années : 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, toutes ensemble.