Formalising Formulas-as-Types-as-Objects. - Qiao Haiyan (TYPES, 1999)

Verifying Haskell Programs by Combining Testing and Proving. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (QSIC, 2003)

Combining Testing and Proving in Dependent Type Theory. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (TPHOLs, 2003)

Formalizing Strong Normalization Proofs of Explicit Substitution Calculi in ALF. - Fairouz Kamareddine; Qiao Haiyan (J. Autom. Reason., 2003)

Testing and Proving in Dependent Type Theory. - Qiao Haiyan (2003)

Random Generators for Dependent Types. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (ICTAC, 2004)

Verifying Haskell programs by combining testing, model checking and interactive theorem proving. - Peter Dybjer; Qiao Haiyan; Makoto Takeyama (Inf. Softw. Technol., 2004)

Testing and Proving Distributed Algorithms in Constructive Type Theory. - Qiao Haiyan (TAP, 2007)