Jules Chouquet (IRIF, Paris Diderot), Normalization by evaluation in MELL proof-nets



With Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco and Lionel Vaux.

We present a way to bound the size of the antireducts in ressource proof-nets (differential nets without boxes), whith respect to the parallel reduction (that is the elimination of an arbitrary number of cuts). This result applies in particular to Taylor expansion of acyclic nets, and leads us to propose a method of normalization by evaluation : we are able to isolate finitely many ressource nets appearing in the relational semantics (that is close to the Taylor expansion) of a net p, and recover its normal form, only whith linear evaluation over these ressource nets.