These seminars are common with the Plume team (ENS Lyon) and are held in the seminar room, second floor of the building Le Chablais, on the Bourget-du-lac (Savoy) site or at ENS Lyon.

Next seminar:

Thursday 12th December 2019 at 10h Variés (Variées),
Séminaire Chocola

The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2020, all years together.

Year 2019

Thursday 12th December 2019 at 10h Variés (Variées),
Séminaire Chocola

Thursday 5th December 2019 at 10h30 Paweł Gładki (Katowice),
Selected applications of algebras with multivalued addition in the algebraic theory of quadratic forms

Abstract: (Hide abstracts)
Hypergroups are objects like groups but with addition taking possibly many values. Likewise, hyperrings and hyperfields are objects similar to rings and fields, but with multivalued addition. Hyperfields provide a convenient tool in axiomatizing the algebraic theory of quadratic forms and in this talk we shall focus on three such applications. Firstly, we shall show how Witt equivalence of fields can be conveniently expressed in the language of hyperfields and will present some recent results on Witt equivalence of function fields over global and local fields. Secondly, we shall show how orderings of higher level can be defined for hyperrings and hyperfields, and, consequently, how they can be used to provide an axiomatic framework to study forms of higher order. Finally, we shall define the category of, so called, presentable fields and define their Witt rings, thus providing yet another machinery to study quadratic forms over fields. The results presented in this talk were obtained jointly with Murray Marshall and Krzysztof Worytkiewicz.

Thursday 14th November 2019 at 10h Variés (Variés),
Séminaire Chocola

Thursday 24th October 2019 at 10h Karim Nour (LAMA),
Normalisation du lambda-mu-mu'-calcul

Abstract: (Hide abstracts)
L'exposé se fera en deux temps. Dans la première partie (accessible à tous les membres de l'équipe), je présenterai le lambda-mu-calcul (pur et typé) de Parigot ainsi que ses propriétés et ses défauts. J'introduirai ensuite le lambda-mu-mu'-calcul (version De Groote) et je vous présenterai ses multiples propriétés de normalisation (sans rentrer dans les détails techniques). Dans la deuxième partie, je reprendrai quelques résultats techniques pour présenter les méthodes que nous avons utilisées pour les démontrer.

Thursday 10th October 2019 at 10h Clovis Eberhart (Tokyo),
History-Dependent Nominal μ-Calculus

Abstract: (Hide abstracts)
The μ-calculus with atoms, or nominal μ-calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history.

Thursday 3rd October 2019 at 10h Karim Nour (LAMA),
Normalisation en λμμ'-calcul

Abstract: (Hide abstracts)
L'exposé se fera en deux temps. Dans la première partie (accessible à tous les membres de l'équipe), je présenterai le lambda-mu-calcul (pure et typé) de Parigot ainsi que ses propriétés et ses défauts. J'introduirai ensuite le lambda-mu-mu'-calcul (version De Groote) et je vous présenterai ses multiples propriétés de normalisation (sans rentrer dans les détails techniques). Dans la deuxième partie, je reprendrai quelques résultats techniques pour présenter les méthodes que nous avons utilisées pour les démontrer.

Thursday 20th June 2019 at 10h Guillaume Geoffroy (Institut de mathématiques de Marseille),
TBA

Abstract: (Hide abstracts)
TBA

Thursday 13th June 2019 at 10h Florent Capelli (Université de Lille),
TBA

Wednesday 12th June 2019 at 10h Dr. Hassen KTHIRI (University of Sfax - Department of Mathematics),
Sur les paires de séries de Pisot dans le corps des séries de Laurent sur un corps fini Fq : Caractérisations et Cardinalités.

Abstract: (Hide abstracts)
L’objectif de ce travail est l’étude algébrique, arithmétique et combinatoire des paires de conjugués des séries à coefficients dans un corps fini, qui sont situés en dehors du cercle unité dont tous les autres conjugués sont á l’intérieur. On s’intéresse principalement à décrire le lien entre les paires des séries de Pisot et leurs constructions. Nous avons montré que les polynômes P(Y) =Yd+Ad−1Yd−1+. . .+A0 ∈ Fq[X][Y] tel que deg(Ad−2)>deg(Ai) pour tout i différent de d−2 et deg(Ad−2)<2 deg(Ad−1) où q différent 2r (r≥1) admet une paire des séries de Laurent. En effet, on étudie la relation entre les polynômes irréductibles, on va prendre à titre d’exemple, le cas des paires des séries des Pisot (ou bien les séries 2-Pisot) tout en déterminant le cardinal de l’ensemble de ces éléments en fonction du degré et de la hauteur logarithmique. Par conséquent, on donne une minoration du nombre des polynômes irréductibles à deux variables sur un corps fini Fq.

Thursday 6th June 2019 at 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Thursday 16th May 2019 at 10h Sergueï Lenglet (Université de Lorraine),
Diacritical Companions

Abstract: (Hide abstracts)
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.

Thursday 9th May 2019 at 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

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

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

Abstract: (Hide abstracts)
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.

Thursday 4th April 2019 at 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Thursday 28th March 2019 at 10h Valentin Blot (Laboratoire Spécification et Vérification (École normale supérieure Paris-Saclay)),
TBA

Abstract: (Hide abstracts)
TBA

Thursday 21st March 2019 at 10h Daniel Martins-Antunes (LAMA),
Digital Curvature Evolution Model for Image Segmentation

Abstract: (Hide abstracts)
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.

Thursday 14th March 2019 at 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

Thursday 14th March 2019 at 10h Guillaume Malod (IMJ-PRJ (Paris 7)),
Séries formelles et calculs non-commutatifs

Abstract: (Hide abstracts)
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.

Thursday 7th February 2019 at 10h Adrien Durier (LIP, ENS Lyon),
Fonctions et processus concurrents

Abstract: (Hide abstracts)
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...

Thursday 24th January 2019 at 10h30 Séminaire Chocola (Plusieurs orateurs),
Voir page web.

The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2020, all years together.