| 2012 | PEPM | Hybrid contract checking via symbolic simplification. | Dana N. Xu |
| 2010 | ATVA | Probabilistic Contracts for Component-Based Design. | Dana N. Xu, Gregor Gler, Alain Girault |
| 2009 | POPL | Static contract checking for Haskell. | Dana N. Xu, Simon L. Peyton Jones, Koen Claessen |
| 2008 | PEPM | A practical and precise inference and specializer for array bound checks elimination. | Corneliu Popeea, Dana N. Xu, Wei-Ngan Chin |
| 2006 | HASKELL | Extended static checking for haskell. | Dana N. Xu |
| 2004 | APLAS | PType System: A Featherweight Parallelizability Detector. | Dana N. Xu, Siau-Cheng Khoo, Zhenjiang Hu |
| 2003 | PEPM | Extending sized type with collection analysis. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |
| 2002 | APLAS | Extending Sized Type with Collection Analysis. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |
| 2002 | APLAS | A Type-Based Approach to Parallelization (preliminary report). | Dana N. Xu, Siau-Cheng Khoo, Wei-Ngan Chin, Zhenjiang Hu |
| 2002 | PEPM | Compiling real time functional reactive programming. | Dana N. Xu, Siau-Cheng Khoo |
| 2001 | APLAS | Higher-Order Polymorphic Sized Types for Safety Checks. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |
| 2000 | APLAS | Deriving Pre-Conditions for Array Bound Check Elimination. | Wei-Ngan Chin, Siau-Cheng Khoo, Dana N. Xu |