2015/02/17 by Marco Solieri
Computer Science · #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.176.7
published as EPTCS 176, 2015, pp. 79-94 · In Proceedings LINEARITY 2014, arXiv:1502.04419
arxiv created 2015/02/17 · arxiv updated 2015/02/18
The Resource λ-calculus is a variation of the λ-calculus where arguments can be superposed and must be linearly used. Hence it is a model for linear and non-deterministic programming languages, and the target language of Ehrhard-Taylor expansion of λ-terms. In a strictly typed restriction of the Resource λ-calculus, we study the notion of path persistence, and we define a Geometry of Interaction that characterises it, is invariant under reduction, and counts addends in normal forms.