Date(s) : 23/10/2014 iCal
11 h 00 min - 12 h 00 min
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 non-deterministic and linear programming languages. But RC is also the target language of Taylor-Ehrhard expansion of λ-terms, a linearisation of the usage of arguments. In a strictly typed restriction of RC, we study the notion of paths on proof-nets 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.
Catégories Pas de Catégories