Intuitionistic Differential Nets and Lambda-Calculus


Paolo Tranquilli


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