Talk "Divergences on computational effects for relational program logics"

by Shin-ya Katsumata

Wed, 07 September 2022 at 12:30 pm in Lipari, Italy

Joint work with: Tetsuya Sato (Tokyo Institute of Technology)

Abstract: Recently, there have been proposed several relational program logics in which relational reasoning about programs is integrated with measurement of quantitative difference between computational effects. Towards a general framework for such relational program logics, we introduce a structure called divergence on monad, which offers a means to measure the distance between two computational effects. We show that divergences on monads induce graded strong relational liftings of monads, which are a key structure for the sound semantics of relational program logics.