dmulligan

18 ms·

1.
by dmulligan 1mo ago
Ha, I actually wrote a paper pushing on this "kernel" pun between OSs and proof-checkers [1], designing a HOL kernel structured like an OS kernel. [1]: https://drops.dagstuhl.de/storage/00lipics/lipics-vo
2.
by dmulligan 3y ago
\documentclass{article} \title{Natural selection in the Health and Retirement Study} \author{XXX} \date{September 2023} \begin{document} \maketitle \begin{abstract} I investigate natural selection on polygenic
3.
by dmulligan 4y ago
I grew up in Greater Manchester, a heavily-industrialised part of the UK, where locally the main industries were at one time coal mining and cotton milling. Members of my family worked in cotton mills, and the machines were so deafening th
4.
by dmulligan 4y ago
It was present in SML codebases earlier than F# (it's used everywhere in the Isabelle codebase, for example, and that's where I first came across it).
5.
by dmulligan 4y ago
That's right!
6.
by dmulligan 4y ago
> It turns out that it is possible if you do it in a special way with locales What was special about it? From memory, the formalisation [1] proceeded exactly how you would expect. Locales are simply an Isabelle mechanism (in addition t
7.
by dmulligan 5y ago
Ha, I'm not sure! I just write papers, the vagaries of how and why journals and conference proceedings are published the way that they are is beyond my ken. Looking back through some of my other papers it seems that there's a mix
8.
by dmulligan 5y ago
See our latest paper [0] for an atomic move operation on replicated trees. [0]: https://dominicpm.github.io/publications/kleppmann-highly-av...
9.
by dmulligan 5y ago
There's a lot of projects working in this area to make enclaves easier to manage and deploy, e.g. Veracruz [0] which I work on. [0]: https://github.com/veracruz-project/veracruz
10.
by dmulligan 7y ago
Arm Research | Security Technical Lead | Cambridge, UK | Fulltime, Onsite Arm Research’s Security group is tasked with securing the Arm architecture, developing new security-related technology, and keeping the rest of Arm informed of curren