
Proof nets and the call-by-value λ-calculus
Keywords: Curry–Howard isomorphism; Call-by-value λ-calculus; Linear logic; Graphical syntaxes; Proof nets; Explicit substitutions; Correctness criteria