| Lem: reusable engineering of real-world semantics DP Mulligan, S Owens, KE Gray, T Ridge, P Sewell ACM SIGPLAN Notices 49 (9), 175-188, 2014 | 104 | 2014 |
| Verifying strong eventual consistency in distributed systems VBF Gomes, M Kleppmann, DP Mulligan, AR Beresford Proceedings of the ACM on Programming Languages 1 (OOPSLA), 1-28, 2017 | 68 | 2017 |
| An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors KE Gray, G Kerneis, D Mulligan, C Pulte, S Sarkar, P Sewell Proceedings of the 48th International Symposium on Microarchitecture, 635-646, 2015 | 46 | 2015 |
| Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques G Dowek, MJ Gabbay, DP Mulligan Logic Journal of IGPL 18 (6), 769-822, 2010 | 42 | 2010 |
| Certified complexity (cerco) RM Amadio, N Ayache, F Bobot, JP Boender, B Campbell, I Garnier, ... Foundational and Practical Aspects of Resource Analysis: Third International …, 2014 | 40 | 2014 |
| The missing link: explaining ELF static linking, semantically S Kell, DP Mulligan, P Sewell Proceedings of the 2016 ACM SIGPLAN International Conference on Object …, 2016 | 31 | 2016 |
| Permissive nominal terms and their unification G Dowek, MJ Gabbay, DP Mulligan Proceedings of the 24th Italian Conference on Computational Logic (CILC’09), 2009 | 24 | 2009 |
| Two-level lambda-calculus MJ Gabbay, DP Mulligan Electronic Notes in Theoretical Computer Science 246, 107-129, 2009 | 17* | 2009 |
| Nominal Henkin Semantics: simply-typed lambda-calculus models in nominal sets MJ Gabbay, DP Mulligan arXiv preprint arXiv:1111.0089, 2011 | 12 | 2011 |
| Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables MJ Gabbay, DP Mulligan Proceedings of the Fourth International Workshop on Logical Frameworks and …, 2009 | 12 | 2009 |
| Confidential Computing—a brave new world DP Mulligan, G Petri, N Spinale, G Stockwell, HJM Vincent 2021 international symposium on secure and private execution environment …, 2021 | 11 | 2021 |
| A highly-available move operation for replicated trees and distributed filesystems M Kleppmann, DP Mulligan, VBF Gomes, AR Beresford Work-in-progress draft. University of Cambridge, 33, 2020 | 10* | 2020 |
| Interleaving anomalies in collaborative text editors M Kleppmann, VBF Gomes, DP Mulligan, AR Beresford Proceedings of the 6th Workshop on Principles and Practice of Consistency …, 2019 | 10 | 2019 |
| Certified complexity R Armadio, A Asperti, N Ayache, B Campbell, D Mulligan, R Pollack, ... Procedia Computer Science 7, 175-177, 2011 | 10 | 2011 |
| Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations Y Hsiao, DP Mulligan, N Nikoleris, G Petri, C Trippel MICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture …, 2021 | 9 | 2021 |
| A framework for establishing strong eventual consistency for conflict-free replicated datatypes VBF Gomes, M Kleppmann, DP Mulligan, AR Beresford Archive of Formal Proofs 2017, 2017 | 9 | 2017 |
| OpSets: Sequential specifications for replicated datatypes (extended version) M Kleppmann, VBF Gomes, DP Mulligan, AR Beresford arXiv preprint arXiv:1805.04263, 2018 | 8 | 2018 |
| Semantic nominal terms MJ Gabbay, DP Mulligan 2nd International Workshop on Theory and Applications of Abstraction …, 2009 | 8 | 2009 |
| One-and-a-halfth order terms: Curry-Howard and incomplete derivations MJ Gabbay, DP Mulligan Logic, Language, Information and Computation: 15th International Workshop …, 2008 | 7 | 2008 |
| On the correctness of an optimising assembler for the intel mcs-51 microprocessor DP Mulligan, C Sacerdoti Coen Certified Programs and Proofs: Second International Conference, CPP 2012 …, 2012 | 4 | 2012 |
Murdoch GabbayLecturer in Computer Science at Heriot-Watt University, Edinburgh, UKVerified email at hw.ac.uk
