Proof nets and the call-by-value lambda-calculus

TL;DR

This paper explores the connection between call-by-value lambda calculus and linear logic proof nets, establishing a strong bisimulation and providing a new algebraic reformulation and correctness criterion for the proof nets.

Contribution

It introduces a detailed correspondence and a new algebraic perspective between call-by-value lambda calculus and proof nets, including a novel correctness criterion.

Findings

Strong bisimulation between calculus and proof nets

Algebraic reformulation of proof nets

New correctness criterion for proof nets

Abstract

This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.