Research Interests:
program verification,
computer security,
programming language semantics,
machine-checked proofs, compilers,
and election technology.
Current work: I work on formally verified numerical methods for scientific computing, and on the technology policy of voting machines and elections.
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
2022-2024 VeriFFI: Verified Foreign Function Interface
2014-2022 CertiCoq: a verified compiler for Coq
2019-2024: Verified Network Toolchain
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.