Labelled Lambda-calculi with Explicit Copy and Erase

Maribel Fernández, Nikolaos Siafakas

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-calculu…