Institut de Mathématiques de Luminy

Abstract 2005-14

Ehrhard Thomas, Regnier Laurent.
Böhm trees, Krivine machine and the Taylor expansion of ordinary lambda-terms.

We show that, given an ordinary lambda-term and a normal resource lambda-term which appears in the normal form of its Taylor expansion, the unique resource term of the Taylor expansion of the ordinary lambda-term reducing to this normal resource term can be obtained by running a version of the Krivine abstract machine.


Last update : july 12, 2005, EL.