Welcome!

I'm a graduate student in the School of Computer Science at Carnegie Mellon University in Pittsburgh, PA. My advisor is Frank Pfenning. I study automated theorem proving and formal mathematics.

Current Projects A Focusing Inverse Method Theorem Prover for LF (Thesis Topic) The Kepler-Code Project A Formaliztion of Galois Theory in Coq

Recent Publications An Interpretation of Isabelle/HOL in HOL Light A Proof-Producing Decision Procedure for Real Arithmetic

Software coq-galois-theory Coq formalization of Galois Theory kepler-code Kepler Conjecture reimplementation ocaml-lib OCaml utilities ocaml-mpfi MPFI interval arithmetic library bindings for OCaml ocaml-cfsqp CFSQP optimization library bindings for OCaml