56 citations · 91 across the 7 of their papers we have counts for
7 papers
Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques
Gilles Dowek, Murdoch J. Gabbay, Dominic Mulligan
Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions…
A modest proposal: explicit support for foundational pluralism
Martin Berger, Dominic P. Mulligan
Whilst mathematicians assume classical reasoning principles by default they often context switch when working, restricting themselves to various forms of subclassical reasoning. Th…
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…
Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets
Murdoch J. Gabbay, Dominic P. Mulligan
We investigate a class of nominal algebraic Henkin-style models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps t…