Divergences on Monads for Relational Program Logics
| Autor: | Sato, Tetsuya, Katsumata, Shin-ya |
|---|---|
| Rok vydání: | 2022 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| DOI: | 10.1017/S0960129523000245 |
| Popis: | Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Towards a general framework for such logics, in this paper, we formalize quantitative difference between computational effects as divergence on monad, then develop a relational program logic acRL that supports generic computational effects and divergences on them. To give a categorical semantics of acRL supporting divergences, we give a method to obtain graded strong relational liftings from divergences on monads. We derive two instantiations of acRL for the verification of 1) various differential privacy of higher-order functional probabilistic programs and 2) difference of distribution of costs between higher-order functional programs with probabilistic choice and cost counting operations. Comment: Preprint |
| Databáze: | arXiv |
| Externí odkaz: |
|