2018/08/10 by Beniamino Accattoli, Accattoli, Beniamino · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · doi:10.48550/arxiv.1808.03395
openalex publication_date 2018/08/10 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
Since the very beginning of the theory of linear logic it is known how to represent the λ-calculus as linear logic proof nets. The two systems however have different granularities, in particular proof nets have an explicit notion of sharing---the exponentials---and a micro-step operational semantics, while the λ-calculus has no sharing and a small-step operational semantics. Here we show that the linear substitution calculus, a simple refinement of the λ-calculus with sharing, is isomorphic to proof nets at the operational level. Nonetheless, two different terms with sharing can still have the same proof nets representation---a further result is the characterisation of the equality induced by proof nets over terms with sharing. Finally, such a detailed analysis of the relationship between terms and proof nets, suggests a new, abstract notion of proof net, based on rewriting considerations and not necessarily of a graphical nature.