Differential logical relations, part II increments and derivatives

Creators: Dal Lago, Ugo; Gavazzo, Francesco

Others:: Alma Mater Studiorum University of Bologna (UNIBO); Foundations of Component-based Ubiquitous Systems (FOCUS) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI) ; Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)

Description

We study the deep relations existing between differential logical relations and incremental computing, by showing how self-differences in the former precisely correspond to derivatives in the latter. We also show how differential logical relations can be seen as a powerful metatheoretical tool in the analysis of incremental computations, enabling an easy proof of soundness of differentiation.

Abstract

International audience

Differential logical relations, part II increments and derivatives

Description

Abstract

Additional details