Differential logical relations, part II increments and derivatives

We study the deep relation existing between differential logical relations and incremental computing by showing how self-differences in the former precisely correspond to derivatives in the latter. The byproduct of such a relationship is twofold: on the one hand, we show how differential logical relations can be seen as a powerful meta-theoretical tool in the analysis of incremental computations, enabling an easy proof of soundness of differentiation. On the other hand, we generalize differential logical relations so as to be able to interpret full recursion, something not possible in the original system