Hongwei Xi

About me Curriculum Vitae (text) (ps)
Contact information Research Statement (text) (ps)
Travel plans PhD Thesis (ps) (ps gzipped) (pdf) (pdf gzipped)
Bibliography Dependent ML


Recent Publications and Drafts

  1. Hongwei Xi, Some Practical Aspects of Dependent Datatypes, November 1999. (draft)

  2. Hongwei Xi and Robert Harper, A Dependently Typed Assembly Language, Technical report OGI-CSE-99-008, July 1999. (bibtex) (ps) (pdf) (extended abstract)

  3. Hongwei Xi and Songtao Xia, Towards Array Bound Check Elimination in Java Virtual Machine Language. In Proceedings of CASCON '99, Mississauga, Ontario, November 1999. (bibtex) (pdf) (ps)

  4. Hongwei Xi, Dependently Typed Data Structures. In Proceedings of Workshop on Algorithmic Aspects of Advanced Programming Languages (WAAAPL '99), Paris, September 1999. (bibtex) (pdf) (ps)

  5. Hongwei Xi and Joachim Steinbach, Erasure for Termination Proofs, Technical report OGI-CSE-99-009, July 1999. (ps)

  6. Hongwei Xi and Frank Pfenning, Dependent Types in Practical Programming. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '99), pp. 214-227, San Antonio, January 1999. (bibtex) (ps) (pdf)

  7. Hongwei Xi, Dead Code Elimination through Dependent Types. In Proceedings of the First International Workshop on Practical Aspects of Declarative Languages (PADL '99), Springer-Verlag LNCS vol. 1551, pp.228-242, San Antonio, January 1999. (bibtex) (ps) (pdf)

  8. Hongwei Xi and Frank Pfenning, Eliminating Array Bound Checking Through Dependent Types. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '98), pp. 249-257, Montreal, June 1998. (bibtex) (ps) (pdf)

  9. Hongwei Xi, Towards automated termination proofs through "Freezing". In Proceedings of 9th International Conference on Rewriting Techniques and Applications (RTA '98), Springer-Verlag LNCS, vol. 1379, pp. 271-285, Japan, April 1998. (bibtex) (ps) (pdf)


Current Research Interests

  1. Dependently Typed Assembly Language. (joint work with Bob Harper)
  2. Array bound check elimination in Java Virtual Machine Language. (joint work with Songtao Xia)
  3. The de Caml compiler.


Fun


Last update: Friday Mar 19 1999

Contact: Hongwei Xi