Computational and Contextual Program Differences: Reasoning About Non-equivalent Effectful Programs in an Higher-Order Scenario
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.
Sun 22 AugDisplayed time zone: Seoul change
16:00 - 17:30 | |||
16:00 30mTalk | Representing Monads with Capabilities HOPE | ||
16:30 30mTalk | Higher-order Programming with Effects and Handlers — with First-Class Functions HOPE Jonathan Immanuel Brachthäuser EPFL, Philipp Schuster University of Tübingen, Edward Lee University of Waterloo, Aleksander Boruch-Gruszecki EPFL | ||
17:00 30mTalk | Computational and Contextual Program Differences: Reasoning About Non-equivalent Effectful Programs in an Higher-Order Scenario HOPE Ugo Dal Lago University of Bologna, Italy / Inria, France, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis |