I am an Assistant Professor at Nanyang Technological University, Singapore. I was previously a Research Fellow at Peterhouse, University of Cambridge. My PhD was supervised by Peter Sewell.

I currently serve as a Chair of the W3C WebAssembly Community Group. WebAssembly is a virtual machine and bytecode which is intended to be a high-performance and portable compilation target. Because it is supported natively by all major Web browsers, any language which compiles to WebAssembly is able to run on the Web!

Conrad Watt

conrad.watt@ntu.edu.sg

Nanyang Technological University
Singapore

Google Scholar
GitHub

Hiring

I have open positions available in Singapore for PhD students and research staff! Please reach out if you're interested in WebAssembly, formal verification, concurrency, or related topics in virtual machines and systems.

Projects

Below is a list of the projects I'm actively working on.

Wasm concurrency

I helped design WebAssembly's initial concurrency specification (Weakening WebAssembly). Due to the restrictions of the Web platform, WebAssembly's initial concurrency features are subject to several limitations, such as an inability to share function pointers between threads. I am now collaborating on a standards proposal (link) to bring richer forms of concurrency to the language.

Mechanisation

Mechanisation is the encoding of a formal model and relevant proofs within a machine-checked theorem prover, producing a particularly rigourous certification of correctness. My mechanisations of the WebAssembly specification have helped to discover bugs in the language's type system, and verify that proposed fixes are correct. I'm continuing to work on mechanisations related to WebAssembly — WasmRef-Isabelle, a verified WebAssembly interpreter, has seen adoption as a fuzzing oracle for the widely-used wasmtime WebAssembly engine (paper).

SpecTec

SpecTec (paper) is a domain-specific language and toolchain for WebAssembly specification. Our ultimate goal is that SpecTec will be a single, normative source of truth for the definition of WebAssembly which generates specification documents, reference implementations, and mechanisations.

Language features for performance

As a young system, WebAssembly lacks several features which are necessary for peak performance, such as direct support for irreducible control flow. If you've been working with WebAssembly and have discovered a performance or expressivity pain point, please reach out!

Publications

Awards

Plain Academic