Dependent types in practical programming H Xi, F Pfenning Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of …, 1999 | 740 | 1999 |

Guarded recursive datatype constructors H Xi, C Chen, G Chen Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of …, 2003 | 364 | 2003 |

Eliminating array bound checking through dependent types H Xi, F Pfenning Proceedings of the ACM SIGPLAN 1998 conference on Programming language …, 1998 | 361 | 1998 |

TPS: a theorem-proving system for classical type theory PB Andrews, M Bishop, S Issar, D Nesmith, F Pfenning, H Xi Journal of automated reasoning 16 (3), 321-353, 1996 | 169 | 1996 |

Combining programming with theorem proving C Chen, H Xi ACM SIGPLAN Notices 40 (9), 66-77, 2005 | 153 | 2005 |

Applied type system H Xi International Workshop on Types for Proofs and Programs, 394-408, 2003 | 146 | 2003 |

A dependently typed assembly language H Xi, R Harper Proceedings of the sixth ACM SIGPLAN international conference on Functional …, 2001 | 134 | 2001 |

Dependent types for program termination verification H Xi Higher-Order and Symbolic Computation 15 (1), 91-131, 2002 | 133 | 2002 |

Imperative programming with dependent types H Xi Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science …, 2000 | 108 | 2000 |

Dependent ML: an approach to practical programming with dependent types H Xi Journal of Functional Programming 17 (2), 215, 2007 | 96 | 2007 |

Perpetual Reductions inλ-Calculus F van Raamsdonk, P Severi, MHB Sørensen, H Xi Information and Computation 149 (2), 173-225, 1999 | 86 | 1999 |

Safe programming with pointers through stateful views D Zhu, H Xi International Workshop on Practical Aspects of Declarative Languages, 83-97, 2005 | 71 | 2005 |

Dead code elimination through dependent types H Xi International Symposium on Practical Aspects of Declarative Languages, 228-242, 1999 | 60 | 1999 |

Meta-programming through typeful code representation C Chen, H Xi ACM SIGPLAN Notices 38 (9), 275-286, 2003 | 50 | 2003 |

Etps: A system to help students write formal proofs PB Andrews, CE Brown, F Pfenning, M Bishop, S Issar, H Xi Journal of Automated Reasoning 32 (1), 75-92, 2004 | 34 | 2004 |

Towards array bound check elimination in Java TM virtual machine language. H Xi, S Xia CASCON 99, 14, 1999 | 33 | 1999 |

Dependently typed data structures H Xi Proceedings of Workshop of Algorithmic Aspects of Advanced Programming …, 1999 | 33 | 1999 |

Upper bounds for standardizations and an application H Xi Journal of Symbolic Logic, 291-303, 1999 | 32 | 1999 |

Dependently typed pattern matching H Xi Journal of universal computer science 9 (8), 851-872, 2003 | 30 | 2003 |

Implementing typeful program transformations C Chen, H Xi Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and …, 2003 | 29 | 2003 |