Qiao Haiyan (ÇÇ Ø¹)

Research interests include type theory and its applications to theorem proving and program verification using the proof assistant Agda/Alfa, security protocol verification, formal methods and formal mathematics.

Some publications

• Verifying Haskell Programs By Combining Testing and Proving, a joint paper with Peter Dybjer and Makoto Takeyama. Proceedings of the Third International Conference on Quality Software, pages 272 - 279, IEEE Computer Society Press, 2003.
• Combining Testing and Proving in Dependent Type Theory, a joint paper with Peter Dybjer and Makoto Takeyama. Proceedings of Theorem Proving in Higher Order Logics, LNCS, Vol. 2758, pages 188 - 203, © Springer-Verlag, 2003.
• Formalising strong normalisation proofs of explicit substitution calculi in ALF, a joint paper with Fairouz Kamareddine. Journal of Automated Reasoning. Volume 30, issues 1, Pages 59-98, 2003. Kluwer Academic Publishers.
• Formalising Formulas-as-Types-as-Objects, Types for Proofs and Programs, International Workshop TYPES'99, LNCS Vol. 1956, p174-193, © Springer-Verlag, 2000.