|
![](images/spacer.gif) |
Vendredi 4 Avril
Heure: |
10:00 - 11:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
De la charactérisation des modèles de H* |
Description: |
Flavien Breuvart Je donnerais une caractérisation (pour une large classe de model du lambda calcul pur) des modèles qui sont pleinement adéquat pour la normalisation de tête, càd dont la théorie est H*. Un K-model extentionel D est pleinement adéquat sii il est hyperimmune, càd que les comportements mal fondés ne sont pas capturées par aucun terme récursif. |
Heure: |
10:00 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
A Core Quantitative Coeffect Calculus |
Description: |
Aloïs Brunel Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this talk, we present a language, called lRPCF, inspired by a generalized interpretation of the exponential modality of bounded linear logic. In lRPCF exponential modalities carry a label--an element of a semiring--providing additional information on how a program uses its context. This additional information is used to express comonadic type analysis. |
|
|