Vendredi 19 Février
Heure: 
11:00  12:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Relational typechecking of connected proofstructures 
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 proofstructure, ? 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 proofstructure, 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. 

