A Deep Inference System for Differential Linear Logic

TL;DR

This paper introduces a deep inference system for differential linear logic without promotion, enabling atomic-level cuts and a normalization process that aligns with sequent calculus translations.

Contribution

It develops a novel deep inference formalism for DiLL without promotion, facilitating atomic cuts and normal form derivations.

Findings

Every provable formula admits a normal form derivation.

Normalization commutes with sequent calculus translation.

System enables fine analysis of resource consumption.

Abstract

Differential linear logic (DiLL) provides a fine analysis of resource consumption in cut-elimination. We investigate the subsystem of DiLL without promotion in a deep inference formalism, where cuts are at an atomic level. In our system every provable formula admits a derivation in normal form, via a normalization procedure that commutes with the translation from sequent calculus to deep inference.