The differential λμ-calculus

We define a differential λμ-calculus which is an extension of both Parigot’s λμ-calculus and Ehrhard–Régnier’s differential λ-calculus. We prove some basic properties of the system: reduction enjoys Church–Rosser and simply typed terms are strongly normalizing.