Abstract

The Resource λ-calculus (RC) is a variation of the λ-calculus, where arguments can be superposed and must be linearly used. Hence it is a model for non-deterministic and linear programming languages, and the target language of the Taylor expansion of λ-terms. In a strictly typed restriction of RC, we study the persistence and we define a Geometry of Interaction that is invariant under reduction, characterises persistence, and counts the addends in normal forms.

Metadata

Type
conference paper
Venue
Electronic Proceedings in Theoretical Computer Science
Event
Linearity 2014,3rd International Workshop on Linearity
Resources
Notes
extended by Geometry of Resource Interaction and Taylor-Ehrhard-Regnier Expansion — A Minimalist Approach
Pages
16
DOI
10.4204/EPTCS.176.7