Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors

Lionel Vaux

It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $\lambda$-terms that this operation commutes with normalization: the expansion of a $\lambda$-term is alwa…