In the folklore of differential linear logic and its denotational models, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cut-elimination.

We make this intuition formal in the context of λ-calculus by introducing a finiteness structure on resource λ-terms, which is such that a λ-term is strongly normalizing iff the support of its Taylor expansion is finitary.

This structure is a refinement of the one introduced by Ehrhard in his LICS 2010 paper: for the latter, we also prove that any strongly normalizing λ-term has a finitary Taylor expansion (this was already known for the terms of system F), but the converse does not hold. As was already the case in Ehrhard's work, the proofs do not rely on any uniformity property, hence this approach is valid for non-deterministic extensions of the λ-calculus as well.

One application of this work is the existence of a normal form for the Taylor expansion of any strongly normalizable term. We will moreover give a brief overview of our work in progress, allowing to extend our results to (must) normalizability and (must) head normalizability : this is the next step in a line of work aiming at a generalization of results by Ehrhard and Regnier [TCS vol. 403, 2008; CiE 2006] that were previously limited to a uniform setting.

(Joint work with Michele Pagani and Christine Tasson.)