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