|
|
 |
|
Mercredi 30 Août
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Coherence for skew near-semiring categories |
| Description: |
Tarmo Uustalu We consider skew near-semiring categories, a relaxation of
near-semiring categories where the unitors, associators, annihilator
and distributor are not required to be natural isomorphisms, they
are just natural transformations in a particular direction. We
prove a coherence theorem for such categories. The theorem states
that, in a free skew near-semiring category over a set of objects,
any two maps between an object and an object in normal form are
equal.
Our main motivating examples for skew near-semiring categories are from programming with effects. While (relative) monads and lax monoidal functors are the same as skew monoids in particular skew monoidal categories, (relative) MonadPlus and Alternative instances are skew near-semiring objects.
This is joint work with Mauro Jaskelioff, Exequiel Rivas and Niccolò Veltri. |
Mardi 5 Septembre
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
On the shape of random Pólya structures |
| Description: |
Michael Wallner |
Mardi 19 Septembre
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
TBA |
| Description: |
Valentin Bonzom |
Vendredi 22 Septembre
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Circular Proofs for Subtyping and Termination |
| Description: |
Rodolphe Lepigre In a recent (submitted) work with Christophe Raffalli, we designed a rich type
system for an extension of System F with subtyping. It includes primitive sums
and products, existential types, and (co-)inductive types. Using a combination
of (pointed) subtyping and circular proofs, we were able to express the system
with typing and subtyping rules that are syntax-directed (up to circularity).
During my talk, I will try to give you a flavour of the techniques we used. In
particular, I will show how choice operators can be used to get rid of typing
contexts, and to allow the commutation of quantifiers with other connectives.
I will then introduce the circular proof framework that is used for handling
inductive and co-inductive types in subtyping rules, and general recursion in
typing rules. |
Vendredi 13 Octobre
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Smooth models of Differential Linear Logic |
| Description: |
Marie Kerjean Differential Linear Logic was constructed following a study of discrete vectorial models of Linear Logic. We want to extend the semantics of Linear Logic in the natural domain of continuous objects and analysis. From the basic fact that Seely's formulas is the direct interpretation of the Kernel Theorem for distributions, we explain two developments :
On one hand we axiomatize a Smooth Differential Linear Logic with a graded syntax where to each solvable Linear partial differential equation one associate an exponential. We construct a model of nuclear Fréchet/ Df spaces for this syntax.
On the other hand, we argue that the interpretation of the $parr$ as Schwartz's epsilon product should be the cornestone of the construction of a smooth classical model of DiLL. From a first-model of $k$-reflexive spaces, and based on pioneering works by Kriegl, Michor and Meise, we construct a variety of (at least two) new models of DiLL. This part is joint work with Y. Dabrowski. |
Vendredi 20 Octobre
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Inlining après l'élimination de fermeture pour OCaml |
| Description: |
Pierre Chambart Usuellement, dans les langages de haut niveau, l'inlining est fait sur
un langage intermédiaire proche d'un lambda calcul, où celà revient
pour les cas simple à de la beta-réduction. Pour diverses raisons,
dans OCaml, nous avons décidé d'introduire un autre langage
intermédiaire où les fermetures sont explicite (flambda) sur lequel
les optimisations haut niveau sont effectuées. Nous discuterons des
avantages et complexités qui viennent avec ce choix. |
Mardi 24 Octobre
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Bijections for Weyl Chamber walks ending on an axis, and arc diagrams |
| Description: |
Mathias Lepoutre |
| Heure: |
15:30 - 18:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
False Beliefs in mathematics |
| Description: |
thé combinatoire |
|
|
