Publications and patents
Click here to go back. See also my Google Scholar and DBLP profiles.
Granted patents
Data security:
Gustavo Federico Petri, Guilhem Floréal Bryant, Dominic Phillip Mulligan, Anthony
Charles Joseph Fox,
US Patent
number 11,836,260,
2023.
System, devices and/or processes for secure computation on a virtual machine:
Dominic Phillip Mulligan, Derek Del Miller, Shale Xiong,
US Patent
number 11,698,980,
2023.
Methods and apparatus for encrypted communication:
Gustavo Federico Petri, Guilhem Floréal Bryant, Dominic Phillip Mulligan, Brendan
James Moran,
US Patent
number 11,658,944,
2023.
Encoding of input to storage circuitry:
Alastair David Reid, Dominic Phillip Mulligan, Milosch Meriac, Matthias Lothar
Boettcher, Nathan Yong Seng Chong, Ian Michael Caulfield, Peter Richard Greenhalgh, Frederic Claude Marie Piry,
Albin Pierrick Tonnerre, Thomas Christopher Grocutt, Yasuo Ishii,
US Patent
number 11,126,714,
2021.
Position papers
Trustworthy AI whitepaper,
Arm Holdings,
2022.
Journal papers
Private delegated computations using strong isolation:
Mathias Brossard, Guilhem Bryant, Basma El Gaabouri, Xinxin Fan, Alexandre
Ferreira, Edmund Grimley Evans, Christopher Haster, Evan Johnson, Derek Miller, Fan Mo, Dominic P Mulligan,
Nick Spinale, Eric Van Hensbergen, Hugo JM Vincent, Shale Xiong,
IEEE Transactions on Emerging Topics in Computing (TETC)
volume 12, issue 1, pages 386–398,
2023.
Link.
A Verification Methodology for the Arm® Confidential Computing Architecture: From
a
Secure Specification to Safe Implementations:
Anthony CJ Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P
Mulligan,
Gustavo Petri, Nathan Chong,
Proceedings of the ACM on Programming Languages (OOPSLA/SPLASH)
volume 7, issue 1, pages 376–405,
2023.
Link.
A highly-available move operation for replicated trees:
Martin Kleppmann, Dominic P Mulligan, Victor BF Gomes, Alastair R
Beresford,
IEEE Transactions on Parallel and Distributed Systems (TPDS)
volume 33, issue 7, pages 1711–1724,
2021.
Link.
Verifying strong eventual consistency in distributed systems:
Victor BF Gomes, Martin Kleppmann, Dominic P Mulligan, Alastair R
Beresford,
Proceedings of the ACM on Programming Languages (OOPSLA/SPLASH)
volume 1, issue OOPSLA, pages 1–28,
2017.
Link.
Lem: reusable engineering of real-world semantics:
Dominic P Mulligan, Scott Owens, Kathryn E Gray, Tom Ridge, Peter
Sewell,
ACM SIGPLAN Notices (ICFP)
volume 49, issue 9, pages 175–188,
2014.
Link.
Permissive nominal terms and their unification: an infinite, co-infinite approach
to
nominal techniques:
Gilles Dowek, Murdoch J Gabbay, Dominic P Mulligan,
Logic Journal of the IGPL
volume 18, issue 6, pages 769–822,
2010.
Link.
Curry-Howard for incomplete first-order logic derivations using one-and-a-half
level
terms:
Murdoch J Gabbay, Dominic P Mulligan,
Information and Computation
volume 208, issue 3, pages 230–258,
2010.
Link.
Two-level lambda-calculus:
Murdoch J Gabbay, Dominic P Mulligan,
Electronic Notes in Theoretical Computer Science
volume 246, pages 107–129,
2009.
Link.
Conference and symposia proceedings
RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security
Verification:
Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P Mulligan, Gustavo Petri,
Christopher W Fletcher, Caroline Trippel,
57th IEEE/ACM International Symposium on Microarchitecture (MICRO)
pages 507–524,
2024.
Link.
All Watched Over by Machines of Loving Grace:
Dominic P Mulligan,
28th International Conference on Types for Proofs and Programs (TYPES)
2023.
Link.
Synthesizing formal models of hardware from RTL for efficient verification of
memory
model implementations:
Yao Hsiao, Dominic P Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline
Trippel,
54th annual IEEE/ACM international symposium on microarchitecture (MICRO)
pages 679–694,
2021.
Link.
Confidential Computing—a brave new world:
Dominic P Mulligan, Gustavo Petri, Nick Spinale, Gareth Stockwell, Hugo JM
Vincent,
International symposium on secure and private execution environment design
(SEED)
pages 132–138,
2021.
Link.
Programming and proving with classical types:
Cristina Matache, Victor BF Gomes, Dominic P Mulligan,
Asian Symposium on Programming Languages and Systems (APLAS)
pages 215–234,
2017.
Link.
The missing link: explaining ELF static linking, semantically:
Stephen Kell, Dominic P Mulligan, Peter Sewell,
Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented
Programming, Systems, Languages, and Applications (OOPSLA/SPLASH)
pages 607–623,
2016.
Link.
An integrated concurrency and core-ISA architectural envelope definition, and
test
oracle, for IBM POWER multiprocessors:
Kathryn E Gray, Gabriel Kerneis, Dominic Mulligan, Christopher Pulte, Susmit
Sarkar, Peter Sewell,
Proceedings of the 48th International Symposium on Microarchitecture
(MICRO)
pages 635–646,
2015.
Link.
On the correctness of an optimising assembler for the Intel MCS-51
microprocessor:
Dominic P Mulligan, Claudio Sacerdoti Coen,
Certified Programs and Proofs: Second International Conference (CPP),
pages 43–59,
2012.
Link.
Workshop papers and abstracts
Privacy-Preserving object detection with Veracruz:
Mathias Brossard, Guilhem Bryant, Xinxin Fan, Alexandre Ferreira, Edmund
Grimley-Evans, Christopher Haster, Derek Miller, Dominic P Mulligan, Hugo JM Vincent, Shale Xiong, Lei
Xu,
IEEE International Conference on Pervasive Computing and Communications
Workshops
and other Affiliated Events (PerCom Workshops)
pages 322–324,
2023.
Link.
Scalable assurance via verifiable hardware-software contracts:
Yao Hsiao, Dominic P Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline
Trippel,
First Workshop on Open-Source Computer Architecture Research (OSCAR)
2022.
Link.
Interleaving anomalies in collaborative text editors:
Martin Kleppmann, Victor BF Gomes, Dominic P Mulligan, Alastair R
Beresford,
Proceedings of the 6th Workshop on Principles and Practice of Consistency for
Distributed Data
pages 1–7,
2019.
Link.
Verifying Strong Eventual Consistency for Conflict-free Replicated Data
Types:
Victor BF Gomes, Martin Kleppmann, Dominic P Mulligan, Alastair R
Beresford,
25th Automated Reasoning Workshop (ARW)
pages 25,
2018.
Link.
Certified complexity (CerCo):
Roberto M Amadio, Nicolas Ayache, François Bobot, Jaap P Boender, Brian
Campbell,
Ilias Garnier, Antoine Madet, James McKinna, Dominic P Mulligan, Mauro Piccolo, Randy Pollack, Yann
Régis-Gianas,
Claudio Sacerdoti Coen, Ian Stark, Paolo Tranquilli,
Foundational and Practical Aspects of Resource Analysis: Third International
Workshop (FOPARA)
pages 1–18,
2014.
Link.
Universal algebra over lambda-terms and nominal terms: the connection in logic
between nominal techniques and
higher-order variables:
Murdoch J Gabbay, Dominic P Mulligan,
Proceedings of the Fourth International Workshop on Logical Frameworks and
Meta-Languages: Theory and Practice (LFMTP)
pages 64–73,
2009.
Link.
Permissive nominal terms and their unification:
Murdoch J Gabbay, Dominic P Mulligan,
Proceedings of the 24th Italian Conference on Computational Logic (CILC)
2009.
Link.
Semantic nominal terms:
Murdoch J Gabbay, Dominic P Mulligan,
2nd International Workshop on Theory and Applications of Abstraction,
Substitution
and Naming (TAASN)
2009.
Link.
One-and-a-halfth order terms: Curry-Howard and incomplete derivations:
Murdoch J Gabbay, Dominic P Mulligan,
International Workshop on Logic, Language, Information, and Computation
(WoLLIC)
pages 179–193,
2008.
Link.
Technical reports and theses
OpSets: Sequential specifications for replicated datatypes (extended
version):
Martin Kleppmann, Victor BF Gomes, Dominic P Mulligan, Alastair R
Beresford,
arXiv,
2018.
Link.
Extensions of Nominal Terms:
Dominic P Mulligan,
PhD thesis, Heriot-Watt University,
2011.
Link.
Unpublished manuscripts
A modest proposal: explicit support for foundational pluralism:
Martin Berger, Dominic P Mulligan,
2023.
Link.
Dijkstra's Algorithm without the distributivity axiom: a proof of correctness in
Agda:
Leonhard D Markert, Dominic P Mulligan,
2016.
Link.
Mosquito: an implementation of higher-order logic:
Dominic P Mulligan,
2013.
Link.
Proof documents
OpSets: Sequential Specifications for Replicated Datatypes:
Martin Kleppmann, Victor BF Gomes, Dominic P Mulligan, Alastair R
Beresford,
Archive of Formal Proofs,
2018.
Link.
A framework for establishing strong eventual consistency for conflict-free
replicated
datatypes:
Victor BF Gomes, Martin Kleppmann, Dominic P Mulligan, Alastair R
Beresford,
Archive of Formal Proofs,
2017.
Link.
The λμ-calculus:
Cristina Matache, Victor BF Gomes, Dominic P Mulligan,
Archive of Formal Proofs,
2017.
Link.