Intuitionistic differential nets and lambda-calculus

We define pure intuitionistic differential proof nets, extending Ehrhard and Regnier's differential interaction nets with the exponential box of Linear Logic. Normalization of the exponential reduction and confluence of the full one is proved. These results are directed and adjusted to give a translation of Boudol's untyped lambda-calculus with resources extended with a linear-nonlinear reduction a la Ehrhard and Regnier's differential lambda-calculus. Such reduction comes in two flavours: baby-step and giant-step beta-reduction. The translation, based on Girard's encoding A -> B similar to !A (sic) B and as such extending the usual one for lambda-calculus into proof nets, enjoys bisimulation for giant-step beta-reduction. From this result we also derive confluence of both reductions. (C) 2010 Elsevier B.V. All rights reserved.