| Dependent types in practical programming H Xi, F Pfenning Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of …, 1999 | 824 | 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 | 147 | 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 | 37 | 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 |
