Geometry of Resource Interaction – A Minimalist Approach

Marco Solieri
(LIPN, Paris 13, Sorbonne Paris Cité, CNRS – DISI, Bologna, INRIA)

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.

In Sandra Alves and Iliano Cervesato: Proceedings Third International Workshop on Linearity (LINEARITY 2014), Vienna, Austria, 13th July, 2014, Electronic Proceedings in Theoretical Computer Science 176, pp. 79–94.
Published: 16th February 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.176.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org