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