We present two rewriting systems that define labelled explicit substitution lambdacalculi. Our work is motivated by the close correspondence between Levy's labelled lambdacalculus and paths in proofnets, which played an important role in the understanding of the Geometry of Interaction. The structure of the labels in Levy's labelled lambdacalculus 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 callbyvalue and callbyname translations of the lambdacalculus into linear logic proofnets.
