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.



Last update : september 17, 2001, EL.