|
|
 |
|
Mardi 4 Juillet
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Random generation of closed lambda-terms |
| Description: |
Maciej Bendkowski |
Vendredi 7 Juillet
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Partiality and container monads |
| Description: |
Niccolò Veltri We investigate monads of partiality in Martin-Löf type theory,
following Moggis general monad-based method for modelling
effectful computations. These monads are often called lifting
monads and appear in category theory with different but related
definitions.
In this talk, we unveil the relation between containers and
lifting monads. We show that the lifting monads usually employed
in type theory can be specified in terms of containers. Moreover,
we give a precise characterization of containers whose
interpretations carry a lifting monad structure. We show that
these conditions are tightly connected with Rosolinis notion of
dominance. We provide several examples, putting particular
emphasis on Caprettas delay monad and its quotiented variant,
the non-termination monad. |
Mardi 11 Juillet
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Sur le diamètre des polytopes en nombres entiers |
| Description: |
Lionel Pournin |
Mardi 18 Juillet
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
clôture de cette année de séminaires & exposés de stagiaires |
| Heure: |
14:30 - 17:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Roger Apéry et l'irrationalité de zêta(3) |
| Description: |
Youssef Abdelaziz |
| Heure: |
15:00 - 18:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Arbres de synchronisation et théorie de la concurrence |
| Description: |
Medhi Naima |
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. |
|
|
