| Dependent types in practical programming H Xi, F Pfenning Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of …, 1999 | 800 | 1999 |
| Eliminating array bound checking through dependent types H Xi, F Pfenning Proceedings of the ACM SIGPLAN 1998 conference on Programming language …, 1998 | 411 | 1998 |
| Guarded recursive datatype constructors H Xi, C Chen, G Chen Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of …, 2003 | 405 | 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 | 189 | 1996 |
| Combining programming with theorem proving C Chen, H Xi ACM SIGPLAN Notices 40 (9), 66-77, 2005 | 155 | 2005 |
| Applied type system H Xi Types for Proofs and Programs: International Workshop, TYPES 2003, Torino …, 2004 | 150 | 2004 |
| Dependent types for program termination verification H Xi Higher-Order and Symbolic Computation 15, 91-131, 2002 | 144 | 2002 |
| A dependently typed assembly language H Xi, R Harper Proceedings of the sixth ACM SIGPLAN international conference on Functional …, 2001 | 144 | 2001 |
| Imperative programming with dependent types H Xi Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science …, 2000 | 115 | 2000 |
| Dependent ml an approach to practical programming with dependent types H Xi Journal of Functional Programming 17 (2), 215-286, 2007 | 104 | 2007 |
| Perpetual Reductions inλ-Calculus F van Raamsdonk, P Severi, MHB Sørensen, H Xi Information and Computation 149 (2), 173-225, 1999 | 89 | 1999 |
| Safe programming with pointers through stateful views D Zhu, H Xi Practical Aspects of Declarative Languages: 7th International Symposium …, 2005 | 77 | 2005 |
| Dead code elimination through dependent types H Xi Practical Aspects of Declarative Languages: First International Workshop …, 1998 | 73 | 1998 |
| Meta-programming through typeful code representation C Chen, H Xi ACM SIGPLAN Notices 38 (9), 275-286, 2003 | 64 | 2003 |
| Towards array bound check elimination in Java TM virtual machine language. H Xi, S Xia CASCON 99, 14, 1999 | 37 | 1999 |
| 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 |
| Upper bounds for standardizations and an application H Xi The Journal of Symbolic Logic 64 (1), 291-303, 1999 | 34 | 1999 |
| Dependently typed data structures H Xi Proceedings of Workshop of Algorithmic Aspects of Advanced Programming …, 1999 | 32 | 1999 |
| Implementing typeful program transformations C Chen, H Xi Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluation and …, 2003 | 31 | 2003 |
| Dependently typed pattern matching H Xi Journal of universal computer science 9 (8), 851-872, 2003 | 31 | 2003 |
