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

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

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

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, 321-353, 1996 | 206 | 1996 |

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

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

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

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

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

Dependent ml an approach to practical programming with dependent types H Xi Journal of Functional Programming 17 (2), 215-286, 2007 | 112 | 2007 |

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

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

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

Meta-programming through typeful code representation C Chen, H Xi ACM SIGPLAN Notices 38 (9), 275-286, 2003 | 70 | 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, 75-92, 2004 | 36 | 2004 |

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

Upper bounds for standardizations and an application H Xi The Journal of Symbolic Logic 64 (1), 291-303, 1999 | 33 | 1999 |

Meta-programming through typeful code representation C Chen, H Xi Journal of functional programming 15 (6), 797-835, 2005 | 32 | 2005 |

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

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