Labelled Lambda-calculi with Explicit Copy and Erase

TL;DR

This paper introduces two labelled explicit substitution lambda-calculi that track exponential information, enhancing the understanding of the Geometry of Interaction and the structure of proof-nets.

Contribution

It presents novel labelled explicit substitution calculi that incorporate exponential information, bridging lambda-calculus and linear logic proof-nets.

Findings

Defined two rewriting systems for labelled explicit substitution lambda-calculi

Connected labels to multiplicative and exponential information in proof-nets

Enhanced understanding of Geometry of Interaction through label structure

Abstract

We present two rewriting systems that define labelled explicit substitution lambda-calculi. Our work is motivated by the close correspondence between Levy's labelled lambda-calculus and paths in proof-nets, which played an important role in the understanding of the Geometry of Interaction. The structure of the labels in Levy's labelled lambda-calculus relates to the multiplicative information of paths; the novelty of our work is that we design labelled explicit substitution calculi that also keep track of exponential information present in call-by-value and call-by-name translations of the lambda-calculus into linear logic proof-nets.