| Dependent types in practical programming H Xi, F Pfenning Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of …, 1999 | 815 | 1999 |
| Eliminating array bound checking through dependent types H Xi, F Pfenning Proceedings of the ACM SIGPLAN 1998 conference on Programming language …, 1998 | 425 | 1998 |
| Guarded recursive datatype constructors H Xi, C Chen, G Chen Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of …, 2003 | 417 | 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 | 205 | 1996 |
| Combining programming with theorem proving C Chen, H Xi ACM SIGPLAN Notices 40 (9), 66-77, 2005 | 158 | 2005 |
| Applied type system H Xi International Workshop on Types for Proofs and Programs, 394-408, 2003 | 151 | 2003 |
| A dependently typed assembly language H Xi, R Harper Proceedings of the sixth ACM SIGPLAN international conference on Functional …, 2001 | 148 | 2001 |
| Dependent types for program termination verification H Xi Higher-Order and Symbolic Computation 15, 91-131, 2002 | 143 | 2002 |
| Imperative programming with dependent types H Xi Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science …, 2000 | 117 | 2000 |
| Dependent ml an approach to practical programming with dependent types H Xi Journal of Functional Programming 17 (2), 215-286, 2007 | 111 | 2007 |
| Perpetual Reductions inλ-Calculus F van Raamsdonk, P Severi, MHB Sørensen, H Xi Information and Computation 149 (2), 173-225, 1999 | 90 | 1999 |
| Safe programming with pointers through stateful views D Zhu, H Xi International Workshop on Practical Aspects of Declarative Languages, 83-97, 2005 | 79 | 2005 |
| Dead code elimination through dependent types H Xi International Symposium on Practical Aspects of Declarative Languages, 228-242, 1999 | 76 | 1999 |
| Meta-programming through typeful code representation C Chen, H Xi ACM SIGPLAN Notices 38 (9), 275-286, 2003 | 69 | 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 | 34 | 1999 |
| Dependently typed data structures H Xi Proceedings of Workshop of Algorithmic Aspects of Advanced Programming …, 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 | 31 | 2003 |
