Differential logical relations, part II increments and derivatives.

• We connect two different fields: differential program semantics and incremental computing. • Program distance is increasingly important for software analysis. • Differential logical relations are a new technique that measures the distance between programs as a third program. • Program derivates are used as a way to achieve incremental computation in higher-order languages. • Program derivates are canonical self-distances and differential logical relations can be used in incremental computing. 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. [ABSTRACT FROM AUTHOR]