Vendredi 19 Février


Retour à la vue des calendrier
Jour Semaine Mois Année
Vendredi 19 Février
Heure: 11:00 - 12:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Relational type-checking of connected proof-structures
Description: Luc Pellissier It is possible to define a typing system for Multiplicative Exponential Linear Logic (MELL): in such a system, typing judgments are of the form ? R : x : ?, where R is a MELL proof-structure, ? is the list of types of the conclusions of R, and x an element of the relational interpretation of ?, meaning that x is an element of the relational interpretation of R (of type ?).
As relational semantics can be used to infer execution properties of the proof-structure, these judgment can be considered as forms of quantitative typing.
We provide an abstract machine that decides, if R satisfies a geometric condition, whether the judgment ? R : x : ? is valid. Also, the machine halts in bilinear time in the sizes of R and x.