Thomas Qu is interested in type theory and software verification.
More contact information is available at the Contact page.