ICFP 2021
Sun 22 - Sat 28 August 2021
Sun 22 Aug 2021 17:00 - 17:30 at HOPE - Session 1

Semantics is traditionally concerned with program equivalence, in which all pairs of programs which are not equivalent are treated the same, and simply dubbed as incomparable. In recent years, various forms of program metrics have been introduced such that the distance between two non-equivalent programs is measured as an element of an appropriate quantale. By letting the underlying quantale to vary as the type of the compared programs become more complex, the recently introduced framework of differential logical relations allows for a new contextual form of reasoning. In this talk, we introduce a generalisation of differential logical relations to effectful higher-order programs, in which not only the values, but also the effects computations produce have to be appropriately distanced in a principled way. In the talk, we discuss the main meta-theoretical properties of our generalisation of differential logical relations and show some of their applications to fields such as approximate computing, differential privacy, and cost analysis.