Séminaire, 23 octobre 2014
Exposés
 11:00: Marco Solieri (Paris 13 (LIPN) / Bologna (Focus)), Geometry of Resource Interaction – A Minimalist Approach

The Resource λcalculus (RC) is a variation of the λcalculus where arguments can be superposed and must be linearly used, and where reduction introduces formal sums on terms. Hence it is a model for nondeterministic and linear programming languages. But RC is also the target language of TaylorEhrhard expansion of λterms, a linearisation of the usage of arguments. In a strictly typed restriction of RC, we study the notion of paths on proofnets and the property of persistency. We define a Geometry of Interaction (GoI) that is invariant under reduction, consequently characterises path persistency, and also accurately counts the number of addends being superposed in normal forms. This work intend to be the first step toward an higher destination: understanding and explicitly describing the relation between expansion and GoI.