Recently my main interest has been refinement types, which combine features of ordinary type systems such as functions and records with elements of program properties such as logical "and". This allows efficient expression of many common program properties that are beyond the scope of ordinary type systems, while retaining desirable properties such as an intuitive error reporting, and efficient checking. My thesis work involves extending the programming language Standard ML with refinement-type checking. Here are some examples of programming with refinement types. See my thesis proposal for more details.
Intersection Types and Computational Effects, International Conference on Functional Programming (ICFP'2000), Montreal, Canada, September 2000. (Joint work with Frank Pfenning.)
A Judgmental Reconstruction of Modal Logic, Mathematical Structures in Computer Science, 11(4), August 2001. (Joint work with Frank Pfenning.)
Modal Types as Staging Specifications for Run-time Code Generation, ACM Computing Surveys, 30(3es), 1998. (Joint work with Philip Wickline, Peter Lee, Frank Pfenning.)
Practical Refinement-Type Checking. Thesis proposal, Carnegie-Mellon University, December 1997.
A Practical Refinement-Type Checker for Standard ML, Algebraic Methodology and Software Technology (AMAST'97), Sydney, Australia, December 1997.
Service Combinators for Web Computing, IEEE Transactions on Software Engineering, 25(3), May/June 1999. (Joint work with Luca Cardelli.)
A Temporal Logic Approach to Binding-Time Analysis, Logic in Computer Science (LICS'96), pages 184-195, July 1996.
A Modal Analysis of Staged Computation, Principles of Programming Languages (POPL'96), pages 258-270, January 1996. A greatly extended version is also available (see above). (joint work with Frank Pfenning).
Graph
domination, tabu search and the football pool problem, Discrete
Applied Mathematics, 74(3):217-228, 1997. (joint work with Gordon
Royle).
