I am interested, broadly speaking, in finding out what
programs are supposed to be doing, and proving that they
actually do what they are supposed to do. In this interplay
of specification and verification, I bring to bear ideas and
techniques from the fields of logic, programming language
theory, type theory, automated deduction and mechanized
My research has focused on low-level code, where
specifications have historically been very murky and vague. My
recent work has been on shared memory concurrency, which on
modern systems leads to subtle memory consistency issues, a
phenomenon called relaxed-memory consistency. I helped clarify
and formalize such widely used systems as the architectures
x86, Power, and ARM, and the new C11/C++11 concurrency model.
For more, here is a complete list
of papers I have written, and here is
a bibliography (bibtex).
- NEW! Shared Memory Concurrency in the Real World: Working with Relaxed Memory Consistency
(slides, pdf) : Invited Tutorial at POPL, Jan'13 (TutorialFest).
- Inventing Abstractions: An academic view on industrial memory models
(slides, pdf) : Invited Talk at REORDER, Jul'12.
- Synchronising C/C++ and POWER
(slides, pdf) : Talk at PLDI, Jun'12.
- Understanding POWER Multiprocesors
(slides, pdf) : Talk at PLDI, Jun'11.
- Multiprocessor Architectures Don't Really Exist (But They Should)
(slides, pdf) : Invited Talk at MTV, Dec'09.
- The Semantics of X86-CC Multiprocessor Machine Code
(slides, pdf) : Talk at POPL, Jan'09.
- Real-World Binding Structures
(slides, pdf) : Talk at WMM, Sep'07.
- Small Proof Witnesses for LF
(slides, ppt) : Talk at ICLP, Oct'05.
- Certified Typechecking in Foundational Certified Code Systems
(slides, ppt) : Talk at Dagstuhl, Sep'04.
- Foundational Certified Code in a Metalogical Framework
(slides, ppt) : Talk at CADE, Aug'03.
- EPSRC EP/H027351: Multiprocessors: From Microarchitecture to Semantic Theory (2010 - 2013): EPSRC Postdoctoral Fellowship in Theoretical Computer Science
- EPSRC EP/F036425: Reasoning with Relaxed Memory Models (2008 - 2012): Sewell, Parkinson, Fraser, Zappa Nardelli, Sarkar
In Feb 2007, I gave
a system aimed at specifying, implementing, and proving
properties of deductive systems, in particular,
programming languages and logics. Materials for the course may be
At Cambridge, I have supervised Types (a part II course) for
the Computer Laboratory, and Semantics of Programming Languages
(a part IB course).
At Carnegie Mellon University, I served as a teaching assistant
for 15-399 (Constructive Logic, a junior/senior year course),
and 15-251 (Great Ideas in Theoretical Computer Science, a
sophomore year course).
Magnus O. Myreen
Milo M. K. Martin
Francesco Zappa Nardelli