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

arXiv: https://arxiv.org/abs/1303.7326 · HTML: https://mlsanity.com/paper/1303.7326/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Mar 2013.

## Built on by (most cited first, 1 of 1)

- [Functorial String Diagrams for Reverse-Mode Automatic Differentiation](https://mlsanity.com/paper/2107.13433/) (2021)

## Abstract (arXiv)

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.