In this talk, we introduce differential logical relations, a new form of logical relation which, in the spirit of metric relations, assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between programs not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity of the compared programs.

After having introduced the notion of a program distance, we will review some of the main notions of program distance offered by the literature and highlight their strengths and weaknesses. We will then introduce differential logical relations, their main properties, and their relationship with the aforementioned notions of program distance. Finally, we will discuss extensions and improvements of the current theory of differential logical relations.