56 citations · 56 across the 3 of their papers we have counts for
4 papers
The Supervisionary proof-checking kernel (or: a work-in-progress towards proof generating code)
Dominic P. Mulligan, Nick Spinale
Interactive theorem proving software is typically designed around a trusted proof-checking kernel, the sole system component capable of authenticating theorems. Untrusted automatio…
Private delegated computations using strong isolation
Mathias Brossard, Guilhem Bryant, Basma El Gaabouri +12
Sensitive computations are now routinely delegated to third-parties. In response, Confidential Computing technologies are being introduced to microprocessors, offering a protected…
OpSets: Sequential Specifications for Replicated Datatypes (Extended Version)
Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan +1
We introduce OpSets, an executable framework for specifying and reasoning about the semantics of replicated datatypes that provide eventual consistency in a distributed system, and…
Verifying Strong Eventual Consistency in Distributed Systems
Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan +1
Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithm…