#### 2007

#### Paolo Tranquilli

#### Abstract

We define pure intuitionistic differential 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 *TeX Embedding failed!*-calculus with multiplicities extended with a linear-non linear reduction à la Ehrhard and Regnier's differential *TeX Embedding failed!*-calculus. Such reduction comes in two flavours: baby-step and giant-step *TeX Embedding failed!*-reduction. The translation, based on Girard's encoding *TeX Embedding failed!* and as such extending the usual one for *TeX Embedding failed!*-calculus into proof nets, enjoys bisimulation for giant-step *TeX Embedding failed!*-reduction. From this result we also derive confluence of both reductions.

#### Download: intudiffnet.pdf

**BibTeX**