The differential lambda-calculus

We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus.

Authors

• Thomas Ehrhard
• Laurent Regnier

Keywords

• Lambda-calculus
• Linear logic
• Denotational semantics
• Linear head reduction