具有显式复制和复制的标号Lambda演算
Labelled Lambda-calculi with Explicit Copy and Erase
摘要：
我们提出了两个重写系统，定义标记显式替换的Alzoda-calculi。我们的工作是出于Levy的标记的代数演算和证明网中的路径之间的密切对应关系，这在相互作用几何的理解中发挥了重要作用。标签的结构在利维的标记的Bendida演算涉及到路径的乘法信息，我们的工作的新颖性是，我们设计的标记明确的替代演算，也保持跟踪指数信息存在于呼叫的按值和呼叫的Bendida演算到线性逻辑证明网的名称翻译。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
