I have been most interested in various forms of Continuations and Control Operators in functional programming languages, and their connection to Type Theory and Logic. Recently, I am also interested in Staged Programming, and Metaprogramming.
Since my PhD Thesis, my interests have been staying in formalization of logical systems for reasoning about programs. Along this line, I studied Calculi for Contexts and for Metavariables, and have been using several Theorem Provers including our own system CAL. I am also interested in theory and practical application of Model Checking.