How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)

Rémy Cerda, Lionel Vaux Auclair

Twenty years after its introduction by Ehrhard and Regnier, differentiation in $\hat{I}»$-calculus and in linear logic is now a celebrated tool. In particular, it allows to establish a T…