Research Interests:
program verification,
computer security,
programming language semantics,
machine-checked proofs, compilers,
and election technology.

My
blog at
Other technology policy work I've done
A bit of history
Public lecture at the University of Illinois in honor of the 40th anniversary of the Four Color Theorem proved by Kenneth Appel and Wolfgang Haken
Previous research projects
2015-2021: The Science of Deep Specification
2013-2017: Formally Verified Cryptography
2006-now: Verified Software Toolchain
2004-2006: Enterprise Network Security Analysis
1997-2005: Foundational Proof-Carrying Code for security of untrusted code.
1986-1996: Standard ML of New Jersey, a compiler for the type-safe functional programming language ML.