The cut-elimination theorem for differential nets with promotion

Abstract

Recently Ehrhard and Regnier have introduced Differential Linear Logic, DiLL for short - an extension of the Multiplicative Exponential fragment of Linear Logic that is able to express non-deterministic computations. The authors have examined the cut-elimination of the promotion-free fragment of DiLL by means of a proofnet-like calculus: differential interaction nets. We extend this analysis to exponential boxes and prove the Cut-Elimination Theorem for the whole DiLL: every differential net that is sequentializable can be reduced to a cut-free net. © 2009 Springer Berlin Heidelberg.