One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations. - Murdoch Gabbay; Dominic P. Mulligan (WoLLIC, 2008)

Two-level Lambda-calculus. - Murdoch James Gabbay; Dominic P. Mulligan (WFLP, 2008)

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables. - Murdoch James Gabbay; Dominic P. Mulligan (LFMTP, 2009)

Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms. - Murdoch James Gabbay; Dominic P. Mulligan (Inf. Comput., 2010)

Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques. - Gilles Dowek; Murdoch James Gabbay; Dominic P. Mulligan (Log. J. IGPL, 2010)

Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets - Murdoch James Gabbay; Dominic P. Mulligan (LFMTP, 2011)

Certified Complexity. - R. Armadio; Andrea Asperti; Nicholas Ayache; Brian Campbell 001; Dominic P. Mulligan; Randy Pollack; Yann Régis-Gianas; Claudio Sacerdoti Coen; Ian Stark (FET, 2011)

Extensions of nominal terms. - Dominic P. Mulligan (2011)

On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. - Dominic P. Mulligan; Claudio Sacerdoti Coen (CPP, 2012)

Corrigendum to "Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms" [Inf.Comput.208(3)(2010) 230-258]. - Murdoch James Gabbay; Dominic P. Mulligan (Inf. Comput., 2012)

Certified Complexity (CerCo). - Roberto M. Amadio; Nicholas Ayache; François Bobot; Jaap Boender; Brian Campbell 001; Ilias Garnier; Antoine Madet; James McKinna; Dominic P. Mulligan; Mauro Piccolo; Randy Pollack; Yann Régis-Gianas; et al. (FOPARA, 2013)

Lem: reusable engineering of real-world semantics. - Dominic P. Mulligan; Scott Owens; Kathryn E. Gray; Tom Ridge; Peter Sewell (ICFP, 2014)

An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. - Kathryn E. Gray; Gabriel Kerneis; Dominic P. Mulligan; Christopher Pulte; Susmit Sarkar; Peter Sewell (MICRO, 2015)

The missing link: explaining ELF static linking, semantically. - Stephen Kell; Dominic P. Mulligan; Peter Sewell (OOPSLA, 2016)

Programming and Proving with Classical Types. - Cristina Matache; Victor B. F. Gomes; Dominic P. Mulligan (APLAS, 2017)

A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes. - Victor B. F. Gomes; Martin Kleppmann; Dominic P. Mulligan; Alastair R. Beresford (Arch. Formal Proofs, 2017)

The LambdaMu-calculus. - Cristina Matache; Victor B. F. Gomes; Dominic P. Mulligan (Arch. Formal Proofs, 2017)

Verifying strong eventual consistency in distributed systems. - Victor B. F. Gomes; Martin Kleppmann; Dominic P. Mulligan; Alastair R. Beresford (Proc. ACM Program. Lang., 2017)

OpSets: Sequential Specifications for Replicated Datatypes. - Martin Kleppmann; Victor B. F. Gomes; Dominic P. Mulligan; Alastair R. Beresford (Arch. Formal Proofs, 2018)

OpSets: Sequential Specifications for Replicated Datatypes (Extended Version). - Martin Kleppmann; Victor B. F. Gomes; Dominic P. Mulligan; Alastair R. Beresford (CoRR, 2018)

Interleaving anomalies in collaborative text editors. - Martin Kleppmann; Victor B. F. Gomes; Dominic P. Mulligan; Alastair R. Beresford (PaPoC@EuroSys, 2019)

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 (MICRO, 2021)

Confidential Computing - a brave new world. - Dominic P. Mulligan; Gustavo Petri; Nick Spinale; Gareth Stockwell; Hugo J. M. Vincent (SEED, 2021)

All Watched Over by Machines of Loving Grace. - Dominic P. Mulligan (TYPES, 2022)

The Supervisionary proof-checking kernel (or: a work-in-progress towards proof generating code). - Dominic P. Mulligan; Nick Spinale (CoRR, 2022)

A Highly-Available Move Operation for Replicated Trees. - Martin Kleppmann; Dominic P. Mulligan; Victor B. F. Gomes; Alastair R. Beresford (IEEE Trans. Parallel Distributed Syst., 2022)

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 J. M. Vincent; Shale Xiong; Lei Xu 012 (PerCom Workshops, 2023)

A modest proposal: explicit support for foundational pluralism. - Martin Berger; Dominic P. Mulligan (CoRR, 2023)

A Verification Methodology for the 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; Nathan Chong (Proc. ACM Program. Lang., 2023)

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 (MICRO, 2024)

Private Delegated Computations Using Strong Isolation. - Mathias Brossard; Guilhem Bryant; Basma El Gaabouri; Xinxin Fan; Alexandre Ferreira; Edmund Grimley-Evans; Christopher Haster; Evan Johnson 001; Derek Miller; Fan Mo; Dominic P. Mulligan; Nick Spinale; et al. (IEEE Trans. Emerg. Top. Comput., 2024)

Careful Whisper: Attestation for peer-to-peer Confidential Computing networks. - Ceren Kocaogullar; Gustavo Petri; Dominic P. Mulligan; Derek Miller; Hugo J. M. Vincent; Shale Xiong; Alastair R. Beresford (CoRR, 2025)