|
|
 |
|
Mardi 15 Mars
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Partitions d'entiers et groupes de Coxeter |
| Description: |
Mathias Pétréolle En 2009, Han a redécouvert et généralisé une identité due à Nekrasovet Okounkov, qui fait un lien entre d'un coté, les puissances de lafonction êta de Dedekind, et de l'autre les partages d'entiers et leurslongueurs d'équerres. Pour cela, il utilise la formule de Macdonald pourle système affine de racines de type A. Je montrerai comment, à l'aidede bijections, il est possible de démontrer des identités deNekrasov-Okounkov pour d'autres types de systèmes de racines (typeaffine C et D notamment), et je présenterai les nouvelles formules deséquerres qui en découlent.Dans une seconde partie, je présenterai la notion d'élémentscycliquement pleinement commutatifs dans les groupes de Coxeter, qui ontété introduits pour étudier une version cyclique d'un théorème deMatsumoto. Je montrerai ensuit comment, en utilisant la théorie desautomates finis, on peut démontrer que la série génératrice de ceséléments est une fraction rationnelle, quelque soit le groupe de Coxeterconsidéré. |
| Heure: |
15:00 - 18:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Treillis cambriens et treillis de Tamari : graphes dirigés et groupes de Coxeter |
| Description: |
François Viard |
Vendredi 18 Mars
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Open Call-by-Value |
| Description: |
Giulio Guerrieri The elegant theory of the call-by-value lambda-calculus relies on
weak evaluation and closed terms, that are natural hypotheses in
the study of programming languages. To model proof assistants,
however, strong evaluation and open terms are required, and it is
well known that the operational semantics of call-by-value becomes
problematic in this case, as first pointed out by Paolini and Ronchi
della Rocca. Here we study the intermediate settingthat we call
Open Call-by-Valueof weak evaluation with open terms, on top
of which Grégoire and Leroy designed the abstract machine of Coq.
Various calculi for Open Call-by-Value already exist, coming from
logical, semantical, or implementative points of view, each one with
its pros and cons. This paper presents a detailed comparative study
of their operational semantics. First, we show that all calculi are
equivalent from a termination point of view, justifying the slogan
Open Call-by-Value. Second, we compare their equational theories.
Third, we present a detailed quantitative analysis of the time cost
model. Four, we introduce a new simple abstract machine, and
prove it a reasonable implementation of Open Call-by-Value with
respect to its cost model. Along the way, there emerges a sharp
deconstruction of call-by-value evaluation and of the complexity of
its implementations.
(Joint work with Beniamino Accattoli) |
|
|
