DominicPM.github.io/publications.html at master · DominicPM/DominicPM.github.io · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
<!DOCTYPE html>
<html>

<head>
  <!-- Google tag (gtag.js) -->
  <script async src="https://www.googletagmanager.com/gtag/js?id=G-003LVMP0GC"></script>
  <script>
    window.dataLayer = window.dataLayer || [];
    function gtag() { dataLayer.push(arguments); }
    gtag('js', new Date());

    gtag('config', 'G-003LVMP0GC');
  </script>

  <title>Publications and patents</title>

  <link rel="stylesheet" href="main.css">

  <meta name="author" content="Dominic Mulligan">
  <meta charset="utf-8">
  <meta name="keywords" content="formal methods, confidential computing, Rust, Isabelle/HOL">
  <meta name="viewport" content="width=device-width, initial-scale=1.0">

  <link rel="preconnect" href="https://fonts.googleapis.com">
  <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
  <link
    href="https://fonts.googleapis.com/css2?family=Cormorant+Garamond:ital,wght@0,300;0,400;0,500;0,600;0,700;1,300;1,400;1,500;1,600;1,700&family=Montserrat:ital,wght@0,100..900;1,100..900&family=Source+Code+Pro:ital,wght@0,200..900;1,200..900&display=swap"
    rel="stylesheet">
</head>

<body>

  <h1>Publications and patents</h1>

  <p>Click <a href="./index.html">here</a> to go back. See also my <a
      href="https://scholar.google.com/citations?hl=en&pli=1&user=LI9Nv6UAAAAJ">Google Scholar</a> and <a
      href="https://dblp2.uni-trier.de/pers/hd/m/Mulligan:Dominic_P=">DBLP</a> profiles.</p>

  <h2>Granted patents</h2>

  <div class="publication">
    <span class="publication-name">Data security</span>:
    <span class="publication-authors">Gustavo Federico Petri, Guilhem Floréal Bryant, Dominic Phillip Mulligan, Anthony
      Charles Joseph Fox</span>,
    <span class="publication-venue">US Patent</span>
    <span class="pubication-meta">number 11,836,260</span>,
    <span class="publication-year">2023</span>.
  </div>

  <div class="publication">
    <span class="publication-name">System, devices and/or processes for secure computation on a virtual machine</span>:
    <span class="publication-authors">Dominic Phillip Mulligan, Derek Del Miller, Shale Xiong</span>,
    <span class="publication-venue">US Patent</span>
    <span class="pubication-meta">number 11,698,980</span>,
    <span class="publication-year">2023</span>.
  </div>

  <div class="publication">
    <span class="publication-name">Methods and apparatus for encrypted communication</span>:
    <span class="publication-authors">Gustavo Federico Petri, Guilhem Floréal Bryant, Dominic Phillip Mulligan, Brendan
      James Moran</span>,
    <span class="publication-venue">US Patent</span>
    <span class="pubication-meta">number 11,658,944</span>,
    <span class="publication-year">2023</span>.
  </div>

  <div class="publication">
    <span class="publication-name">Encoding of input to storage circuitry</span>:
    <span class="publication-authors">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</span>,
    <span class="publication-venue">US Patent</span>
    <span class="pubication-meta">number 11,126,714</span>,
    <span class="publication-year">2021</span>.
  </div>

  <h2>Position papers</h2>

  <div class="publication">
    <span class="publication-name">Trustworthy AI whitepaper</span>,
    <span class="publication-authors">Arm Holdings</span>,
    <span class="publication-year">2022</span>.
  </div>

  <h2>Journal papers</h2>

  <div class="publication">
    <span class="publication-name">Private delegated computations using strong isolation</span>:
    <span class="publication-authors">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</span>,
    <span class="publication-venue">IEEE Transactions on Emerging Topics in Computing (TETC)</span>
    <span class="pubication-meta">volume 12, issue 1, pages 386&ndash;398</span>,
    <span class="publication-year">2023</span>.
    <a href="./publications/brossard-private-2022.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">A Verification Methodology for the Arm® Confidential Computing Architecture: From
      a
      Secure Specification to Safe Implementations</span>:
    <span class="publication-authors">Anthony CJ Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P
      Mulligan,
      Gustavo Petri, Nathan Chong</span>,
    <span class="publication-venue">Proceedings of the ACM on Programming Languages (OOPSLA/SPLASH)</span>
    <span class="pubication-meta">volume 7, issue 1, pages 376&ndash;405</span>,
    <span class="publication-year">2023</span>.
    <a href="./publications/fox-verification-2023.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">A highly-available move operation for replicated trees</span>:
    <span class="publication-authors">Martin Kleppmann, Dominic P Mulligan, Victor BF Gomes, Alastair R
      Beresford</span>,
    <span class="publication-venue">IEEE Transactions on Parallel and Distributed Systems (TPDS)</span>
    <span class="pubication-meta">volume 33, issue 7, pages 1711&ndash;1724</span>,
    <span class="publication-year">2021</span>.
    <a href="./publications/kleppmann-highly-available-2021.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Verifying strong eventual consistency in distributed systems</span>:
    <span class="publication-authors">Victor BF Gomes, Martin Kleppmann, Dominic P Mulligan, Alastair R
      Beresford</span>,
    <span class="publication-venue">Proceedings of the ACM on Programming Languages (OOPSLA/SPLASH)</span>
    <span class="pubication-meta">volume 1, issue OOPSLA, pages 1&ndash;28</span>,
    <span class="publication-year">2017</span>.
    <a href="./publications/gomes-verifying-2017.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Lem: reusable engineering of real-world semantics</span>:
    <span class="publication-authors">Dominic P Mulligan, Scott Owens, Kathryn E Gray, Tom Ridge, Peter
      Sewell</span>,
    <span class="publication-venue">ACM SIGPLAN Notices (ICFP)</span>
    <span class="pubication-meta">volume 49, issue 9, pages 175&ndash;188</span>,
    <span class="publication-year">2014</span>.
    <a href="./publications/mulligan-lem-2014.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Permissive nominal terms and their unification: an infinite, co-infinite approach
      to
      nominal techniques</span>:
    <span class="publication-authors">Gilles Dowek, Murdoch J Gabbay, Dominic P Mulligan</span>,
    <span class="publication-venue">Logic Journal of the IGPL</span>
    <span class="pubication-meta">volume 18, issue 6, pages 769&ndash;822</span>,
    <span class="publication-year">2010</span>.
    <a href="./publications/dowek-permissive-2011.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Curry-Howard for incomplete first-order logic derivations using one-and-a-half
      level
      terms</span>:
    <span class="publication-authors">Murdoch J Gabbay, Dominic P Mulligan</span>,
    <span class="publication-venue">Information and Computation</span>
    <span class="pubication-meta">volume 208, issue 3, pages 230&ndash;258</span>,
    <span class="publication-year">2010</span>.
    <a href="./publications/gabbay-one-2009.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Two-level lambda-calculus</span>:
    <span class="publication-authors">Murdoch J Gabbay, Dominic P Mulligan</span>,
    <span class="publication-venue">Electronic Notes in Theoretical Computer Science</span>
    <span class="pubication-meta">volume 246, pages 107&ndash;129</span>,
    <span class="publication-year">2009</span>.
    <a href="./publications/gabbay-two-2009.pdf">Link.</a>
  </div>

  <h2>Conference and symposia proceedings</h2>

  <div class="publication">
    <span class="publication-name">RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security
      Verification</span>:
    <span class="publication-authors">Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P Mulligan, Gustavo Petri,
      Christopher W Fletcher, Caroline Trippel</span>,
    <span class="publication-venue">57th IEEE/ACM International Symposium on Microarchitecture (MICRO)</span>
    <span class="pubication-meta">pages 507&ndash;524</span>,
    <span class="publication-year">2024</span>.
    <a href="./publications/hsiao-rtl-2024.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">All Watched Over by Machines of Loving Grace</span>:
    <span class="publication-authors">Dominic P Mulligan</span>,
    <span class="publication-venue">28th International Conference on Types for Proofs and Programs (TYPES)</span>
    <span class="publication-year">2023</span>.
    <a href="./publications/mulligan-all-2023.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Synthesizing formal models of hardware from RTL for efficient verification of
      memory
      model implementations</span>:
    <span class="publication-authors">Yao Hsiao, Dominic P Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline
      Trippel</span>,
    <span class="publication-venue">54th annual IEEE/ACM international symposium on microarchitecture (MICRO)</span>
    <span class="pubication-meta">pages 679&ndash;694</span>,
    <span class="publication-year">2021</span>.
    <a href="./publications/hsiao-synthesizing-2021.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Confidential Computing—a brave new world</span>:
    <span class="publication-authors">Dominic P Mulligan, Gustavo Petri, Nick Spinale, Gareth Stockwell, Hugo JM
      Vincent</span>,
    <span class="publication-venue">International symposium on secure and private execution environment design
      (SEED)</span>
    <span class="pubication-meta">pages 132&ndash;138</span>,
    <span class="publication-year">2021</span>.
    <a href="./publications/mulligan-confidential-2021.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Programming and proving with classical types</span>:
    <span class="publication-authors">Cristina Matache, Victor BF Gomes, Dominic P Mulligan</span>,
    <span class="publication-venue">Asian Symposium on Programming Languages and Systems (APLAS)</span>
    <span class="pubication-meta">pages 215&ndash;234</span>,
    <span class="publication-year">2017</span>.
    <a href="./publications/matache-programming-2017.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">The missing link: explaining ELF static linking, semantically</span>:
    <span class="publication-authors">Stephen Kell, Dominic P Mulligan, Peter Sewell</span>,
    <span class="publication-venue">Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented
      Programming, Systems, Languages, and Applications (OOPSLA/SPLASH)</span>
    <span class="pubication-meta">pages 607&ndash;623</span>,
    <span class="publication-year">2016</span>.
    <a href="./publications/kell-missing-2016.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">An integrated concurrency and core-ISA architectural envelope definition, and
      test
      oracle, for IBM POWER multiprocessors</span>:
    <span class="publication-authors">Kathryn E Gray, Gabriel Kerneis, Dominic Mulligan, Christopher Pulte, Susmit
      Sarkar, Peter Sewell</span>,
    <span class="publication-venue">Proceedings of the 48th International Symposium on Microarchitecture
      (MICRO)</span>
    <span class="pubication-meta">pages 635&ndash;646</span>,
    <span class="publication-year">2015</span>.
    <a href="./publications/gray-integrated-2015.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">On the correctness of an optimising assembler for the Intel MCS-51
      microprocessor</span>:
    <span class="publication-authors">Dominic P Mulligan, Claudio Sacerdoti Coen</span>,
    <span class="publication-venue">Certified Programs and Proofs: Second International Conference (CPP)</span>,
    <span class="pubication-meta">pages 43&ndash;59</span>,
    <span class="publication-year">2012</span>.
    <a href="./publications/mulligan-correctness-2012.pdf">Link.</a>
  </div>

  <h2>Workshop papers and abstracts</h2>

  <div class="publication">
    <span class="publication-name">Privacy-Preserving object detection with Veracruz</span>:
    <span class="publication-authors">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</span>,
    <span class="publication-venue">IEEE International Conference on Pervasive Computing and Communications
      Workshops
      and other Affiliated Events (PerCom Workshops)</span>
    <span class="pubication-meta">pages 322&ndash;324</span>,
    <span class="publication-year">2023</span>.
    <a href="./publications/bryant-privacy-2023.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Scalable assurance via verifiable hardware-software contracts</span>:
    <span class="publication-authors">Yao Hsiao, Dominic P Mulligan, Nikos Nikoleris, Gustavo Petri, Caroline
      Trippel</span>,
    <span class="publication-venue">First Workshop on Open-Source Computer Architecture Research (OSCAR)</span>
    <span class="publication-year">2022</span>.
    <a href="./publications/hsiao-scalable-2022.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Interleaving anomalies in collaborative text editors</span>:
    <span class="publication-authors">Martin Kleppmann, Victor BF Gomes, Dominic P Mulligan, Alastair R
      Beresford</span>,
    <span class="publication-venue">Proceedings of the 6th Workshop on Principles and Practice of Consistency for
      Distributed Data</span>
    <span class="pubication-meta">pages 1&ndash;7</span>,
    <span class="publication-year">2019</span>.
    <a href="./publications/kleppmann-interleaving-2019.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Verifying Strong Eventual Consistency for Conflict-free Replicated Data
      Types</span>:
    <span class="publication-authors">Victor BF Gomes, Martin Kleppmann, Dominic P Mulligan, Alastair R
      Beresford</span>,
    <span class="publication-venue">25th Automated Reasoning Workshop (ARW)</span>
    <span class="pubication-meta">pages 25</span>,
    <span class="publication-year">2018</span>.
    <a href="./publications/gomes-verifying-2018.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Certified complexity (CerCo)</span>:
    <span class="publication-authors">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</span>,
    <span class="publication-venue">Foundational and Practical Aspects of Resource Analysis: Third International
      Workshop (FOPARA)</span>
    <span class="pubication-meta">pages 1&ndash;18</span>,
    <span class="publication-year">2014</span>.
    <a href="./publications/amadio-certified-2013.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Universal algebra over lambda-terms and nominal terms: the connection in logic
      between nominal techniques and
      higher-order variables</span>:
    <span class="publication-authors">Murdoch J Gabbay, Dominic P Mulligan</span>,
    <span class="publication-venue">Proceedings of the Fourth International Workshop on Logical Frameworks and
      Meta-Languages: Theory and Practice (LFMTP)</span>
    <span class="pubication-meta">pages 64&ndash;73</span>,
    <span class="publication-year">2009</span>.
    <a href="./publications/gabbay-universal-2009.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Permissive nominal terms and their unification</span>:
    <span class="publication-authors">Murdoch J Gabbay, Dominic P Mulligan</span>,
    <span class="publication-venue">Proceedings of the 24th Italian Conference on Computational Logic (CILC)</span>
    <span class="publication-year">2009</span>.
    <a href="./publications/dowek-permissive-2009.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Semantic nominal terms</span>:
    <span class="publication-authors">Murdoch J Gabbay, Dominic P Mulligan</span>,
    <span class="publication-venue">2nd International Workshop on Theory and Applications of Abstraction,
      Substitution
      and Naming (TAASN)</span>
    <span class="publication-year">2009</span>.
    <a href="./publications/gabbay-semantic-2009.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">One-and-a-halfth order terms: Curry-Howard and incomplete derivations</span>:
    <span class="publication-authors">Murdoch J Gabbay, Dominic P Mulligan</span>,
    <span class="publication-venue">International Workshop on Logic, Language, Information, and Computation
      (WoLLIC)</span>
    <span class="pubication-meta">pages 179&ndash;193</span>,
    <span class="publication-year">2008</span>.
    <a href="./publications/gabbay-one-2008.pdf">Link.</a>
  </div>

  <h2>Technical reports and theses</h2>

  <div class="publication">
    <span class="publication-name">OpSets: Sequential specifications for replicated datatypes (extended
      version)</span>:
    <span class="publication-authors">Martin Kleppmann, Victor BF Gomes, Dominic P Mulligan, Alastair R
      Beresford</span>,
    <span class="publication-venue">arXiv</span>,
    <span class="publication-year">2018</span>.
    <a href="https://arxiv.org/abs/1805.04263">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Extensions of Nominal Terms</span>:
    <span class="publication-authors">Dominic P Mulligan</span>,
    <span class="publication-venue">PhD thesis, Heriot-Watt University</span>,
    <span class="publication-year">2011</span>.
    <a href="./publications/mulligan-extensions-2011.pdf">Link.</a>
  </div>

  <h2>Unpublished manuscripts</h2>

  <div class="publication">
    <span class="publication-name">A modest proposal: explicit support for foundational pluralism</span>:
    <span class="publication-authors">Martin Berger, Dominic P Mulligan</span>,
    <span class="publication-year">2023</span>.
    <a href="https://arxiv.org/abs/2302.10137">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Dijkstra's Algorithm without the distributivity axiom: a proof of correctness in
      Agda</span>:
    <span class="publication-authors">Leonhard D Markert, Dominic P Mulligan</span>,
    <span class="publication-year">2016</span>.
    <a href="./publications/markhert-dijkstra-2016.pdf">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">Mosquito: an implementation of higher-order logic</span>:
    <span class="publication-authors">Dominic P Mulligan</span>,
    <span class="publication-year">2013</span>.
    <a href="./publications/mulligan-mosquito-2013.pdf">Link.</a>
  </div>

  <h2>Proof documents</h2>

  <div class="publication">
    <span class="publication-name">OpSets: Sequential Specifications for Replicated Datatypes</span>:
    <span class="publication-authors">Martin Kleppmann, Victor BF Gomes, Dominic P Mulligan, Alastair R
      Beresford</span>,
    <span class="publication-venue">Archive of Formal Proofs</span>,
    <span class="publication-year">2018</span>.
    <a href="https://www.isa-afp.org/entries/OpSets.html">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">A framework for establishing strong eventual consistency for conflict-free
      replicated
      datatypes</span>:
    <span class="publication-authors">Victor BF Gomes, Martin Kleppmann, Dominic P Mulligan, Alastair R
      Beresford</span>,
    <span class="publication-venue">Archive of Formal Proofs</span>,
    <span class="publication-year">2017</span>.
    <a href="https://www.isa-afp.org/entries/LambdaMu.html">Link.</a>
  </div>

  <div class="publication">
    <span class="publication-name">The λμ-calculus</span>:
    <span class="publication-authors">Cristina Matache, Victor BF Gomes, Dominic P Mulligan</span>,
    <span class="publication-venue">Archive of Formal Proofs</span>,
    <span class="publication-year">2017</span>.
    <a href="https://www.isa-afp.org/entries/CRDT.html">Link.</a>
  </div>

</body>