Formal verification of authenticated, append-only skip lists in Agda. - Victor Cacciari Miraldo; Harold Carr; Mark Moir; Lisandra Silva; Guy L. Steele Jr. (CPP, 2021)

Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version. - Victor Cacciari Miraldo; Harold Carr; Mark Moir; Lisandra Silva; Guy L. Steele Jr. (CoRR, 2021)

Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. - Harold Carr; Christa Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (NFM, 2022)

Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version. - Harold Carr; Christopher Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (CoRR, 2022)

An approach to translating Haskell programs to Agda and reasoning about them. - Harold Carr; Christa Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (CoRR, 2022)