Parallel Reduction in Resource Lambda-Calculus

We study the resource calculus – the non-lazy version of Boudol’s λ-calculus with resources. In such a calculus arguments may be finitely available and mixed, giving rise to nondeterminism, modelled by a formal sum. We define parallel reduction in resource calculus and we apply, in such a nondeterministic setting, the technique by Tait and Martin-L¨of to achieve confluence. Then, slightly generalizing a technique by Takahashi, we obtain a standardization result.

• Type: Conference
• Year: 2009
• Where: APLAS
• Authors: Michele Pagani, Paolo Tranquilli
• Keywords: APLAS 2009, Calculus Arguments, Non-lazy Version, Resource Calculus