I am a Computer Scientist in the Center for Applied Scientific Computing (CASC) at Lawrence Livermore National Laboratory (LLNL). My research interests are in the fields of programming languages and applied formal methods, which generally involves reasoning about the behavior of computer programs and systems using mathematical techniques.

My recent work is on binary analysis, building certified systems in the Coq proof assistant, and making Coq proofs easier. I am broadly interested in the application of PL/FM to systems, networking, and security; and on easing the burden of certified programming.

My personal research website can be found at https://goto.ucsd.edu/~john. It is not sanctioned or supported by the DOE, UC, LLNL, or any other organization.

Postdoc, Cornell University, Ithaca, NY

Ph.D. and M.S., Computer Science, UC San Diego, San Diego, CA

B.S., Mathematics and Computer Science, Harvey Mudd College, Claremont, CA