1 paper
Christa Jenkins, Mark Moir, Harold Carr
We present a lightweight, open source Agda framework for manually verifying effectful programs using predicate transformer semantics. We represent the abstract syntax trees (AST) o…