Research Interests
My current interests are program verification and type theory. I am also interested more generally in functional programming, language implementation, and program analysis. Theorem provers are totally sweet.
My advisor is Ranjit Jhala. God help him.
Papers
Liquid Types; Ming Kawaguchi, Ranjit Jhala; PLDI 2008
Software
Oyices
Oyices is an OCaml binding for the yices theorem prover. The binding is an overlay over the yices Linux binary distribution.