19 citations · 28 across the 6 of their papers we have counts for
6 papers
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…
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…
Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version
Harold Carr, Christopher Jenkins, Mark Moir +2
LibraBFT is a Byzantine Fault Tolerant (BFT) consensus protocol based on HotStuff. We present an abstract model of the protocol underlying HotStuff / LibraBFT, and formal, machine-…
Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version
Victor Cacciari Miraldo, Harold Carr, Mark Moir +2
Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify th…
Enhancing Accountability and Trust in Distributed Ledgers
Maurice Herlihy, Mark Moir
Permisionless decentralized ledgers ("blockchains") such as the one underlying the cryptocurrency Bitcoin allow anonymous participants to maintain the ledger, while avoiding contro…
Hardware extensions to make lazy subscription safe
Dave Dice, Timothy L. Harris, Alex Kogan +2
Transactional Lock Elision (TLE) uses Hardware Transactional Memory (HTM) to execute unmodified critical sections concurrently, even if they are protected by the same lock. To ensu…