Deriving Pre-Conditions for Array Bound Check Elimination. - Wei-Ngan Chin; Siau-Cheng Khoo; Dana N. Xu (APLAS, 2000)

Higher-Order Polymorphic Sized Types for Safety Checks. - Wei-Ngan Chin; Siau-Cheng Khoo; Dana N. Xu (APLAS, 2001)

Extending Sized Type with Collection Analysis. - Wei-Ngan Chin; Siau-Cheng Khoo; Dana N. Xu (APLAS, 2002)

A Type-Based Approach to Parallelization (preliminary report). - Dana N. Xu; Siau-Cheng Khoo; Wei-Ngan Chin; Zhenjiang Hu (APLAS, 2002)

Compiling real time functional reactive programming. - Dana N. Xu; Siau-Cheng Khoo (ASIA-PEPM, 2002)

PType System: A Featherweight Parallelizability Detector. - Dana N. Xu; Siau-Cheng Khoo; Zhenjiang Hu (APLAS, 2004)

Extended static checking for haskell. - Dana N. Xu (Haskell, 2006)

A practical and precise inference and specializer for array bound checks elimination. - Corneliu Popeea; Dana N. Xu; Wei-Ngan Chin (PEPM, 2008)

Static contract checking for Haskell. - Dana N. Xu; Simon L. Peyton Jones; Koen Claessen (POPL, 2009)

Hybrid contract checking via symbolic simplification. - Dana N. Xu (PEPM, 2012)

Probabilistic contracts for component-based design. - Gregor Gößler; Dana N. Xu; Alain Girault (Formal Methods Syst. Des., 2012)