Institut
de Mathématiques de Luminy

Abstract 2001-30 |

**Ehrhard** Thomas and **Regnier**
Laurent.

The differential lambda-calculus

We present an extension of the lambda-calculus with differential constructions motivated by a model of linear logic discovered by the first author and presented in [Ehr01]. We state and prove some basic results (confluence, weak normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus. |