加载中…
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.

生成讲解博客的中文版本

生成AI智能校验的中文版本