I am a Ph.D. candidate in Computer Science Department at Portland State University advised by professor Tim Sheard. My thesis research is about theories and language design for a logically consistent system that is convienent for both functional programming and logical reasoning, based on the Curry--Howard correspondence. My research interests, other than my thesis, are on programming languages: type systems, automated testing (using solvers), formal verification, subtyping for algebraic datatypes, and other aspects of functional languages. See my CV for details.
See my Google Scholar profile.