## Publications

Click here for my DBLP entry and here for my Google Scholar entry.

# Journals

*Private delegated computations using strong isolation*. Accepted in ***IEEE Transactions on Emerging Topics in Computer Science**, 2023. To appear. PDF*A highly-available move operation for replicated trees*. Martin Kleppmann, Dominic P. Mulligan, Victor Gomes, and Alastair Beresford.**IEEE Transactions on Parallel and Distributed Systems**, volume 33, issue 7, pages 1711–1734, 2021. PDF*Permissive nominal terms and their unification: an infinite, coinfinite approach to nominal techniques.*Gilles Dowek, Murdoch J. Gabbay, and Dominic P. Mulligan.**Logic Journal of the Interest Group in Pure Logic**, volume 18, issue 6, pages 769–822, 2011. PDF*Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms.*Murdoch J. Gabbay and Dominic P. Mulligan.**Journal of Information and Computation, volume 208**, issue 3, pages 230–258, 2010. PDF

# Conferences and workshops

*All watched over by machines of loving grace*. Dominic P. Mulligan.**Accepted into the TYPES 2022 post-proceedings**, 2023. PDF*A verification methodology for Arm Confidential Computing Architecture, from a secure specification to safe implementations*. Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, and Nathan Chong.**Accepted at OOPSLA/SPLASH**, 2023. PDF*Scalable assurance via verifiable hardware-software contracts.*Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline Trippel.**Accepted at the 1st Workshop on Open-source Computer Architecture Research (OSCAR)**, 2022. PDF*The Supervisionary proof-checking kernel: or, a work-in-progress towards proof-generating code.*Dominic P. Mulligan, Nick Spinale.**Accepted at the 6th Workshop on Principles of Secure Compilation (PriSC)**, 2022. PDF*Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations.*Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, and Caroline Trippel.**Accepted at the 54th IEEE/ACM International Symposium on Microarchitecture (MICRO)**, 2021. PDF*Seeds of SEED: Confidential Computing—a brave new world (invited industry paper).*Dominic P. Mulligan, Gustavo Petri, Nick Spinale, Gareth Stockwell, and Hugo J. M. Vincent.**Accepted at the IEEE International Symposium on Secure and Private Execution Environment Design (SEED)**, 2021. PDF*Interleaving anomalies in collaborative text editors.*Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan, and Alastair R. Beresford.**Proceedings of the 6th Workshop on the Principles and Practice of Consistency for Distributed Data (PaPoC)**, 2019. PDF*Programming and proving with classical types.*Cristina Matache, Victor B. F. Gomes, and Dominic P. Mulligan.**Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS)**, pages 215–234, 2017. PDF*Verifying Strong Eventual Consitency in distributed systems.*Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford.**Proceedings of PACMPL/OOPSLA**, 109:1–109:28, 2017.*Distinguished paper award.**Distinguished artefact award.*PDF*The missing link: explaining ELF static linking, semantically.*Stephen Kell, Dominic P. Mulligan, and Peter Sewell.**Proceedings of the ACM SIGPLAN International Conference on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA/SPLASH)**, pages 607–623, 2016. PDF*An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors.*Kathryn Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar and Peter Sewell.**Proceedings of the 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO 48)**, pages 635–646, 2015. PDF*Lem: reusable engineering of real world semantics.*Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell.**Proceedings of the 19th International Conference on Functional Programming (ICFP)**, pages 175–188, 2014. PDF*Certified Complexity (CerCo).*Roberto M. Amadio, Nicolas Ayache, Francois 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, and Paolo Tranquilli.**Proceedings of the 3rd International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA)**, pages 1–18, 2013. PDF*On the correctness of an assembler for the MCS-51 microprocessor.*Dominic P. Mulligan and Claudio Sacerdoti Coen.**Proceedings of the 2nd International Conference on Certified Proofs and Programs (CPP)**, pages 43–59, 2012. PDF*Nominal Henkin Semantics: simply typed lambda-calculus in Nominal Sets.*Murdoch J. Gabbay and Dominic P. Mulligan.**Proceedings of the 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP)**, pages 58–75, 2011. PDF*Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables.*Murdoch J. Gabbay and Dominic P. Mulligan.**Proceedings of the 4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP)**, pages 64–73, 2009. PDF*The two-level lambda-calculus.*Murdoch J. Gabbay and Dominic P. Mulligan.**Electronic Notes in Theoretical Computer Science**, volume 246, pages 107–129, 2009. PDF*Permissive nominal terms and their unification.*Gilles Dowek, Murdoch J. Gabbay and Dominic P. Mulligan.**Presented at the 24th Convegno Italiano di Logica Computazionale (CILC)**, 2009. PDF*Semantic nominal terms.*Murdoch J. Gabbay and Dominic P. Mulligan.**Presented at the 2nd International Workshop on the Theory and Applications of Abstraction, Substitution and Naming (TAASN)**, 2009. PDF*One-and-a-half level terms: Curry-Howard for incomplete derivations.*Murdoch J. Gabbay and Dominic P. Mulligan.**Proceedings of the 15th International Workshop on Logic, Language, Information and Computation (WoLLIC)**, pages 179–193, 2008. PDF

# Formal developments

*The lambda-mu calculus.*Cristina Matache, Victor B. F. Gomes, and Dominic P. Mulligan.**Archive of Formal Proofs**, 2017.*A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes.*Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford.**Archive of Formal Proofs**, 2017.

# Thesis

*Extensions of nominal terms*. Dominic P. Mulligan, PhD thesis,**Heriot-Watt University**, 2011. PDF

# Posters

*Certified complexity.*Roberto Amadio, Andrea Asperti, Nicolas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Regis-Giannas, Claudio Sacerdoti Coen and Ian Stark.**Presented at the EU Future and Emerging Technologies Exhibition**, 2011. PDF

# Drafts, technical reports, and manuscripts

*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 J. M. Vincent, Shale Xiong. Arm Research technical report, 2022. PDF*Dijkstra’s algorithm without the distributivity axiom: a proof of correctness in Agda.*Leonhard D. Markert and Dominic P. Mulligan, 2016. PDF*Mosquito: an implementation of higher-order logic (rough diamond).*Dominic P. Mulligan, 2013. PDF*Permissive nominal terms.*Gilles Dowek, Murdoch J. Gabbay, and Dominic P. Mulligan.**INRIA technical report 6682**, 2008. PDF