2 papers
cs.SE2022
Proof Engineering with Predicate Transformer Semantics
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…
cs.LO2022
An approach to translating Haskell programs to Agda and reasoning about them
Harold Carr, Christa Jenkins, Mark Moir +2
We are using the Agda programming language and proof assistant to formally verify the correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / LibraBF…