Relational type-checking for MELL proof-structures. Part 1: Multiplicatives

Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco

Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered.…