Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Hongwei Xi
[go: Go Back, main page]
     
Home
Contact Information
Weekly Calendar
Curriculum Vitæ
Research Interests
Publications
Projects
ATS
Xanadu
Dependent ML
Courses
Intro to CS II [Spring 07]
PPL [Fall 06]
Intro to CS II [Spring 06]
CPL [Fall 05]
Compiler [Spring 05]
CPL [Fall 04]
Compiler [Spring 04]
PPL [Fall 03]
CAD [Spring 03]
PPL [Fall 02]
CPL [Spring 02]
  

Hongwei Xi
Publications

Journals

  1. Hongwei Xi, Dependent ML: an approach to practical programming with dependent types, Journal of Functional Programming (JFP), vol. 17(2), pp. 215-286, March 2007. (pdf) (ps)

  2. Chiyan Chen, Rui Shi and Hongwei Xi, Implementing Typeful Program Transformations, Fundamenta Informaticae, vol. 69 (1-2), pp. 103-121. (bibtex) (pdf) (ps)

  3. Chiyan Chen and Hongwei Xi, Meta-Programming through Typeful Code Representation, Journal of Functional Programming, vol. 15(6), pp. 797--835, 2005. (bibtex) (pdf) (ps)

  4. Peter B. Andrews, Matthew Bishop, Chad Brown, Sunil Issar, Frank Pfenning and Hongwei Xi, ETPS: A System to Help Students Write Formal Proofs, Journal of Automated Reasoning (JAR), vol. 32(1), pp. 75--92, 2004. (pdf) (ps)

  5. Hongwei Xi, Dependently Typed Pattern Matching, Journal of Universal Computer Science (JUCS), 9(8), pp. 851-872, August 2003. (bibtex) (pdf) (ps)

  6. Hongwei Xi, Dependent Types for Program Termination Verification, Journal of Higher-Order Symbolic Computation, 15(1), pp. 91--131, March 2002. (bibtex) (pdf) (ps)

  7. Femke van Raamsdonk, Paula Severi, Morten H. Sorensen and Hongwei Xi, Perpetual Reductions in Lambda-Calculus, Journal of Information and Computation, 149(2), pp. 173--225, March 1999. (bibtex) (pdf) (ps)

  8. Hongwei Xi, Upper bounds for standardisation and an application, Journal of Symbolic Logic, 64(1), pp. 291--303, March 1999. (bibtex) (pdf) (ps)

  9. Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi, TPS: A Theorem Proving System for Classical Type Theory, Journal of Automated Reasoning, 16(3), pp. 321--353, 1996. (bibtex) (pdf)

  10. Hongwei Xi, Half-Closed Intervals of Rescursively Enumerable Degrees (in Chinese with English abstract), Math. Semiannuals of Nanjing University, P.R. China, 1989.

Conferences and Symposiums

  1. Rui Shi, Chiyan Chen and Hongwei Xi, Distributed Meta-Programming. In Proceedings of the 5th International Conference on Generative Programming and Component Engineering (GPCE'06), Portland, OR, October 2006. (bibtex) (pdf) (ps) (slides in ppt)

  2. Chiyan Chen and Hongwei Xi, Combining Programming with Theorem Proving. In Proceedings of the 10th International Conference on Functional Programming (ICFP'05), Tallinn, Estonia, September 2005. (bibtex) (pdf) (ps) (slides in pdf)

  3. Dengping Zhu and Hongwei Xi, Safe Programming with Pointers through Stateful Views. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages (PADL'05), Springer-Verlag LNCS vol. 3350, pp. 83--97, Long Beach, CA, January 2005. (bibtex) (pdf) (ps) (slides in ppt)

  4. Chiyan Chen, Rui Shi and Hongwei Xi, A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. In Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages (PADL'04), Springer-Verlag LNCS vol. 3057, pp. 23--38, Dallas, TX, June 2004. (bibtex) (pdf) (ps) (slides in ppt)

  5. Chiyan Chen, Dengping Zhu and Hongwei Xi, Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell. In Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages (PADL'04), Springer-Verlage LNCS vol. 3057, pp. 239--254, Dallas, TX, June 2004. (bibtex) (pdf) (ps) (slides in ppt)

  6. Dengping Zhu and Hongwei Xi, A Typeful and Tagless Representation for XML Documents. In Proceedings of the First Asian Symposium on Programming Languages and Systems (APLAS'03), Springer-Verlag LNCS vol. 2895, pp. 89--104, Beijing, China, November 2003. (bibtex) (pdf) (ps)

  7. Walid Taha, Stephan Ellner and Hongwei Xi, Generating Imperative, Heap-Bounded Programs in a Functional Setting. In Proceedings of the Third International Conference on Embedded Software (EMSOFT'03), Springer-Verlag LNCS vol. 2855, pp. 340--355, Philadelphia, PA, October 2003. (bibtex) (pdf) (ps)

  8. Hongwei Xi, Facilitating Program Verification with Dependent Types. In Proceedings of International Conference on Software Engineering and Formal Methods (SEFM'03), pp. 72--81, Brisbane, Australia, September 2003. (bibtex) (pdf) (ps) (slides in ppt)

  9. Chiyan Chen and Hongwei Xi, Meta-Programming through Typeful Code Representation. In Proceedings of the 8th International Conference on Functional Programming (ICFP'03), pp. 275--286, Uppsala, Sweden, August 2003. (bibtex) (pdf) (ps) (slides in ppt)

  10. Hongwei Xi, Dependently Typed Pattern Matching. In Proceedings of Simposio Brasileiro de Linguagens de Programacao (SBLP'03), pp. 149--165, Ouro Preto, Brazil, May 2003. (bibtex) (pdf) (ps) (slides in ppt)

  11. Hongwei Xi, Chiyan Chen and Gang Chen, Guarded Recursive Datatype Constructors. In Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'03), pp. 224--235, New Orleans, Louisiana, January 2003. (bibtex) (pdf) (ps) (slides in ppt)

  12. Hongwei Xi, Unifying Object-Oriented Programming with Typed Functional Programming, ASIAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (ASIA-PEPM'02), pp. 117--125, Aizu-Wakamatsu, Japan, September 2002. (bibtex) (pdf) (ps)

  13. Hongwei Xi and Robert Harper, Dependently Typed Assembly Language. In Proceedings of the 6th International Conference on Functional Programming (ICFP'01), pp. 169--180, Florence, September 2001. (bibtex) (pdf) (ps)

  14. Hongwei Xi, Dependent Types for Program Termination Verification. In Proceedings of 16th Symposium on Logic in Computer Science (LICS'01), pp. 231--242, Boston, June 2001. (bibtex) (pdf) (ps)

  15. Hongwei Xi, Imperative Programming with Dependent Types, In Proceedings of 15th Symposium on Logic in Computer Science (LICS'00), pp. 375--387, Santa Barbara, June 2000. (bibtex) (pdf) (ps)

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

  17. 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) (pdf) (ps)

  18. 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) (pdf) (ps)

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

  20. Hongwei Xi, Evaluation under lambda-abstraction. In Proceedings of 9th International Symposium on Programming Languages, Implementations, Logics, and Programs (PLILP'97), Springer-Verlage LNCS 1292, pp. 259--273, Southampton, UK, September 1997. (bibtex) (pdf) (ps)

  21. Hongwei Xi, Upper bounds for standardisation and an application. In the proceedings of Kurt Gödel Colloquium 1997 (KGC'97), Springer-Verlag LNCS, vol. 1289, pp. 335--348, Vienna, August 1997. (bibtex) (pdf) (ps)

  22. Hongwei Xi, Simulating Eta-Expansions with Beta-Reductions in the Second-Order Polymorphic Lambda-Calculus. In the proceedings of Symposium on Logical Foundations of Computer Science (LFCS'97), Springer-Verlag LNCS, vol. 1234, pp. 399--409, Yaroslavl, July 1997. (bibtex) (pdf) (ps)

  23. Hongwei Xi, Weak and Strong Beta Normalisations in Typed Lambda-Calculi. In the proceedings of Typed Lambda Calculi and Applications (TLCA'97), Springer-Verlag LNCS, vol. 1210, pp. 390--404, April 1997. (bibtex) (pdf) (ps)

Workshops

  1. Kevin Donnelly and Hongwei Xi, A Formalization of Strong Normalization for Simply Typed Lambda-Calculus and System F. International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Seattle, WA, August 2006. (bibtex) (pdf) (ps)

  2. Kevin Donnelly and Hongwei Xi, System Description: Combining Higher-Order Abstract Syntax with First-Order Abstract Syntax in ATS. International Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'05), Tallinn, Estonia, September 2005. (bibtex) (pdf) (ps)

  3. Sa Cui and Kevin Donnelly and Hongwei Xi, ATS: a language that combines programming with theorem proving. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems, (FroCos'05), Springer-Verlag LNCS 3717, pp. 310--320, Vienna, Austria, September 2005. (bibtex) (pdf) (ps)

  4. Hongwei Xi, Development Separation in Lambda-Calculus, In Proceedings of the 12th Workshop on Logic, Language, Information and Computation (WoLLIC'05), ENTCS vol. 143, pp. 207--221, Florianopolis, Santa Catarina, Brazil, July 2005. (bibtex) (pdf) (ps) (slides in pdf)

  5. Hongwei Xi, Applied Type System (extended abstract). In the post-workshop proceedings of TYPES 2003, Springer-Verlag LNCS vol. 3085, pp. 394--408, 2004. (bibtex) (pdf) (ps) (full paper: pdf ps)

  6. Chiyan Chen and Hongwei Xi, Implementing Typeful Program Transformations, ACM SIGPLAN 2003 Workshop on Partial Evaluation and Semantics Based Program Manipulation (PEPM'03), pp. 20--28, San Diego, CA, June 2003. (bibtex) (pdf) (ps)

  7. Hongwei Xi and Carsten Schuermann, CPS Transform for Dependent ML (abstract). In the meeting report of the 8th Workshop on Logic, Language, Information and Computation (WoLLIC'01), Logic Journal of IGPL, 9(5), pp. 739--754, Brasilia, Brazil, August 2001. (bibtex) (pdf) (ps)

  8. Hongwei Xi, Dependently Typed Data Structures. In Proceedings of the Workshop on Algorithmic Aspects of Advanced Programming Languages (WAAAPL'99), pp. 17--32, Paris, September 1999. (bibtex) (pdf) (ps) (slides in ppt) (full paper: pdf ps)

  9. 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) (pdf) (ps)

  10. Hongwei Xi, Generalized Lambda-Calculi (abstract). In the meeting report of the 4th Workshop on Logic, Language, Information and Computation (WoLLIC'97), Logic Journal of IGPL, 5(6), pp. 925--927, Fortaleza(Ceara), Brazil, August 1997. (bibtex) (pdf) (ps)

  11. Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi, TPS: An interactive and automatic tool for proving theorems of type theory, In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, pages 366-370, Vancouver, B.C., Canada, August 1993. Springer-Verlag LNCS 780. (bibtex) (ps)

  12. Hongwei Xi, On branching and nonbranching recursively enumerable degrees (in Chinese), National Logic Workshop, Shantou University, China, October, 1990.

Technical Reports

  1. Hongwei Xi and Dengping Zhu and Yanka Li, Applied Type System with Stateful Views, Technical Report, no. BUCS-2005-03, Computer Science Department, Boston University, January, 2005. (pdf) (ps)

  2. Hongwei Xi and Joachim Steinbach, Erasure for Termination Proofs, Technical Report OGI-CSE-99-009, Oregon Graduate Institute, August 1999.

  3. Hongwei Xi and Robert Harper, A Dependently Typed Assembly Language, Technical Report OGI-CSE-99-008, Oregon Graduate Institute, July 1999.

  4. Joachim Steinbach and Hongwei Xi, Freezing -- Termination Proofs for Classical, Context-Sensitive and Innermost Rewriting, January 1998

  5. Hongwei Xi, On weak and strong normalisations, Research Report 96-187, Mathematics Department, Carnegie Mellon University, 1996.

  6. Hongwei Xi, An induction measure on lambda-terms and its applications, Research Report 96-192, Mathematics Department, Carnegie Mellon University, 1996.

Manuscripts

  1. Hongwei Xi, Dependent Types in Practical Programming (Ph.D thesis), September, 1998

  2. Hongwei Xi, Combining Algebraic Rewriting with Second Order Extentional Polymorphic Lambda Calculus, October, 1996

    [ Home | Contact | CV | Research | Publication ]
    [ Projects | Courses ]

    hwxi AT cs DOT bu DOT edu
    http://www.cs.bu.edu/~hwxi