PLClub Discussion Group

Dijkstra Monads Forever

This Friday, I will be presenting Steve and I’s 2021 POPL paper Dijkstra Monad’s Forever. I will be discussing Dijkstra Monads, a framework for representing specifications over effectful programming languages, and how the approach to Interaction Trees. This approach can encode both partial correctness and total correctness logics, as well as (usefully) richer specifications. In this talk, I will show how we can use this approach to write verifiable specifications for programs whose intended behavior is to output some infinite sequence of observable events.

For homework, please either introduce yourself to or brush up on Interaction Trees by Xia, et al. A link to the paper and a recording of the talk can be found at this link https://popl20.sigplan.org/details/POPL-2020-Research-Papers/14/Interaction-Trees-Representing-Recursive-and-Impure-Programs-in-Coq.