------------------------------------------
Hongwei Xi
Associate Professor
Computer Science Department
Boston University
111 Cummington Street
Boston, MA 02215
Office: +1 (617) 358-2511
Fax: +1 (617) 353-6457
Email: hwxi@cs.bu.edu
Url: http://www.cs.bu.edu/~hwxi/
- * - * - * - * - * - * ------------------------------------------
Education:
Ph.D. in Carnegie Mellon University
Pure & Applied Logic Pittsburgh, USA
December 1998 GPA: 3.98 / 4.00
M.S. in Nanjing University
Mathematics Nanjing, China
July 1988 GPA: 3.60 / 4.00
B.S. in Nanjing University
Mathematics Nanjing, China
June 1985 GPA: 3.70 / 4.00
- * - * - * - * - * - * ------------------------------------------
Applicable Skills:
Software Development Operating systems, Networking, Parallel
computing, Program verification, User
Interface.
Programming Languages ATS, C, C++, JAVA, PERL, LISP, FORTRAN
Platforms Most versions of Unix, Windows NT, TCP/IP,
Motif, Mach
- * - * - * - * - * - * ------------------------------------------
Academic Experience:
Associate Professor Computer Science Department
09/07 to present Boston University
Assistant Professor Computer Science Department
10/01 to 08/07 Boston University
Assitant Professor Department of ECE & CS
09/99 to 10/01 University of Cincinnati
Post-doc Researcher Department of Computer Science & Engineering
08/98 to 08/99 Oregon Graduate Institute
Doctoral Thesis Dependent Types in Practical Programming
02/96 to 08/98 This work strengthens the current type system
of the functional programming language ML with
a restricted form of dependent types. It not only
provides the programmer with significantly more
information to catch program errors at compile-
time, but also enables the compiler writer to
obtain type information for optimizing code
generation. As an significant application, we
have shown how to eliminate array bound checks
in real code. Please check out some interesting
examples in
http://www.cs.cmu.edu/~hwxi/DML/examples/
I have finished a prototype implementation of
the system, which is running successfully.
Instructor Carnegie Mellon Action Program
Summer 1997 An introductory calculus course
for minority students
Instructor Department of Mathematical Sciences, CMU
Summer 1996 and 1997 Calculus II for Humanities and Social Sciences
Teaching Assistant Department of Mathematical Sciences, CMU
09/94 to present Calculus I & II, Calculus in 3 Dimensions
Introduction to Modern Math.
Research Assistant Department of Mathematical Sciences, CMU
06/92 to 08/94 Professor Peter Andrews
Summer 95 Maintaining and improving a large theorem
proving system TPS, which consists of more
than 100,000 lines of code written in LISP
Assistant Professor Department of Computer Science,
Shanghai Jiao Tong University, China
07/88 to 06/92 Responsible for teaching Mathematical Logic
and Discrete Math at undergraduage level,
and Type Theory at graduate level. Also
responsible for the design of a programming
language based on equational reasoning and
supervising undergraduate students during
their interns.
- * - * - * - * - * - * ------------------------------------------
Relevant Experience:
Consultant The 8th Construction Company, Shanghai
Designing a graphics system on PC for
drawing construction flowcharts and
monitoring construction schedules
Consultant The Construction Branch of Bao Shan Steel
Factory, Shanghai
Using software monitoring the construction
of the NO. 3 furnace in Bao Shan steel
factory, which was the largest in China.
- * - * - * - * - * - * ------------------------------------------
Selected Courses: All taken at Carnegie Mellon University
Computer Science Programming languages, Operating system,
Computer Architecture, Algorithm,
Artificial Intelligence
Mathematics Real analysis, Abstract algebra, Topology,
Functional Analysis, Mathematical Logic
Statistics Advanced probability I & II
Advanced statistics I & II
- * - * - * - * - * - * ------------------------------------------
Papers on line:
Publications http://www.cs.bu.edu/~hwxi/publications.html
- * - * - * - * - * - * ------------------------------------------
Refereed Papers
Publication in Journals:
^^^^^^^^^^^^^^^^^^^^^^^
06. Hongwei Xi, Dependently Typed Pattern Matching, Journal of
Universal Computer Science (JUCS), 9(8), pp. 851-872,
August 2003.
05. Hongwei Xi, Dependent Types for Program Termination
Verification, Journal of Higher-Order Symbolic Computation
(HOSC), 15(1), pp. 91--131, March 2002.
04. Femke van Raamsdonk, Paula Severi, Morten H. Sorensen and
Hongwei Xi, Perpetual Reductions in lambda-calculus,
Journal of Information and Computation (IC), 149(2),
pp. 173--225, 1999.
03. Hongwei Xi, Upper bounds for standardisation and an application,
Journal of Symbolic Logic (JSL), 64(1), pp. 291--303, March 1999.
02. 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.
01. Hongwei Xi. On recursively enumerable degrees(in Chinese with
English abstract), Math. Semiannual of Nanjing University,
China, 1989.
Publication in Conferences:
^^^^^^^^^^^^^^^^^^^^^^^^^^
18. 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), Beijing, China,
November 2003.
17. 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), Philadelphia, PA, October 2003.
16. 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.
15. Chiyan Chen and Hongwei Xi, Meta-Programming through Typeful
Code Representation. In Proceedings of International Conference
on Functional Programming (ICFP '03), pp. 275--286, Uppsala,
Sweden, August 2003.
14. 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.
13. 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.
12. Hongwei Xi, Unifying Object-Oriented Programming with Typed
Functional Programming, ASIAN Symposium on Partial Evaluation
and Semantics-Based Program Manipulation (ASIA-PEPM),
pp. 117--125, Aizu-Wakamatsu, Japan, September 2002.
11. Hongwei Xi and Robert Harper, A Dependently Typed Assembly
Language, International Conference on Functional Programming
(ICFP '01), pp. 169--180, Florence, September 2001
10. Hongwei Xi, Dependent Types for Program Termination Verification,
In Proceedings of 16th IEEE Symposium on Logic in Computer Science
(LICS '01), pp. 231--242, Boston, June 2001.
09. Imperative Programming with Dependent Types, In Proceedings of
15th IEEE Symposium on Logic in Computer Science (LICS '00),
Santa Barbara, June 2000.
08. Hongwei Xi and Songtao Xia, Towards Array Bound Check Elimination
in Java Virtual Machine Language, In Proceedings of CASCON '99,
Mississauga, Ontario, November 1999.
07. 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, Texas, January 1999.
06. 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.
05. Hongwei Xi, Towards automated termination proofs through
"Freezing". In Proceedings of 9th International Conference on
Rewriting Techniques and Applications (RTA '98), LNCS, vol. 1379,
pp. 271--285, Japan, April 1998.
04. Hongwei Xi, Evaluation under lambda-abstraction. In Proceedings
of 9th International Symposium on Programming Languages,
Implementations, Logics, and Programs (PLILP '97),
LNCS, vol. 1292, pp. 259--273.
03. Hongwei Xi, Simulating Eta-Expansions with Beta-Reductions
in the Second-Order Polymorphic Lambda-Calculus. In Proceedings
of Symposium on Logical Foundations of Computer Science (LFCS '97),
LNCS, vol. 1234, pp. 399--409, July, Yaroslavl, 1997.
02. Hongwei Xi, Upper bounds for standardisation and an application.
In Proceedings of Kurt Gödel Colloquium '97 (KGC '97), LNCS,
vol. 1289, pp. 335--348, September 1997.
01. Hongwei Xi, Weak and Strong Beta Normalisations in Typed
Lambda-Calculi. In Proceedings of Typed Lambda Calculi and
Applications (TLCA '97), LNCS, vol. 1210, pp. 390--404,
April 1997.
Publication in Workshops:
^^^^^^^^^^^^^^^^^^^^^^^^
07. 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.
06. 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), Brasilia, Brazil, August 2001.
05. Hongwei Xi, Dependently Typed Data Structures. In Proceedings
of Workshop on Algorithmic Aspects of Advanced Programming
Languages (WAAAPL '99), Paris, September 1999.
04. Hongwei Xi, Dead Code Elimination through Dependent Types, the
First International Workshop on Practical Aspects of Declarative
Languages (PADL '99), San Antonio, January, 1999.
03. 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, Springer-Verlag LNCS 780},
pp. 366-370, Vancouver, August, 1993.
02. Hongwei Xi. Generalized Lambda-Calculi}(abstract). In the meeting
report of the 4th Workshop on Logic, Language, Information and
Computation (WoLLIC), Logic Journal of IGPL, 5(6), pp. 925-927
Fortaleza(Ceara), Brazil, August, 1997.
01. Hongwei Xi. On branching and nonbranching recursively
enumerable degrees(in Chinese), National Logic Conference,
Shantou University, China, October, 1990.
- * - * - * - * - * - * ------------------------------------------
Unrefereed Papers
Technical Reports:
^^^^^^^^^^^^^^^^^
1. Hongwei Xi. On Weak and Strong Normalizations. Research Report
96-187, Mathematics Department, Carnegie Mellon University, 1996.
2. Hongwei Xi. An Induction Measure on Lambda-Terms and Its
Applications. Research Report 96-192, Department of Mathematical
Sciences, 1996.
Manuscripts:
^^^^^^^^^^^
1. Hongwei Xi. Combining Algebraic Rewriting with Second Order
Extensional Polymorphic Lambda Calculus, October, 1996.
2. Hongwei Xi. Separating Developments, October, 1996.
3. Joachim Steinbach and Hongwei Xi. Freezing -- Termination for
Classical, Context-Sensitive and Innermost Rewriting, January,
1998.
- * - * - * - * - * - * ------------------------------------------
Conference Presentations:
09. Hongwei X and Chiyan Chen, Meta-Programming through Typeful
Code Representation, the 8th International Conference on
Functional Programming (ICFP '03), Uppsala, Sweden, August 2003.
08. Hongwei Xi and Chiyan Chen and Gang Chen, Guarded Recursive
Datatype Constructors, the 30th ACM SIGPLAN Symposium on
Principles of Programming Languages (POPL '03), New Orleans,
Louisiana, January 2003.
07. Hongwei Xi and Robert Harper, A Dependently Typed Assembly
Language, International Conference on Functional Programming
(ICFP '01), pp. 169--180, Florence, September 2001
06. Hongwei Xi, Dependent Types for Program Termination Verification,
the 16th IEEE SIGPLAN Symposium on Logic in Computer Science
(LICS '01), Boston, MA, June 2001.
05. Hongwei Xi, Imperative Programming with Dependent Types,
the 15th IEEE SIGPLAN Symposium on Logic in Computer Science
(LICS '00), Santa Barbara, CA, June 2000.
04. Hongwei Xi, Dependent Types in Practical Programming, ACM
SIGPLAN Symposium on Principles of Programming Languages (POPL),
San Antonio, January 1999.
03. Hongwei Xi, Dead Code Elimination through Dependent Types, First
International Workshop on Practical Aspects of Declarative
Languages, San Antonio, January 1999.
02. Hongwei Xi, Eliminating Array Bound Checking Through Dependent
Types, ACM SIGPLAN conference on Programming Language Design and
Implementation (PLDI), Montreal, June 1998.
01. Matthew Bishop and Hongwei Xi, The ETPS Educational Theorem
Proving System, The 8th Annual Computing and Philosophy
Conference (CAP), Pittsburgh, August, 1993.
- * - * - * - * - * - * ------------------------------------------
Invited Talks:
09. Hongwei Xi, Unifying Object-Oriented Programming with Typed
Functional Programming, Computer Science Department,
Rice University, Houston, TX, 16 & 18 April 2003.
08. Hongwei Xi, Unifying Object-Oriented Programming with Typed
Functional Programming, ASIAN Symposium on Partial Evaluation
and Semantics-Based Program Manipulation (ASIA-PEPM),
Aizu-Wakamatsu, Japan, 14 September 2002.
07. Hongwei Xi, Implementing Staged Computation, Information
Processing Laboratory, Department of Information Engineering
and Department of Mathematical Science and Informatics,
University of Tokyo, Tokyo, Japan, 11 September 2002.
06. Hongwei Xi, Dependent Types for Program Termination Verification,
Computer Science Department, Yale University, 13 June 2001.
05. Hongwei Xi, Compiling with Dependent Types, Workshop
on Proof-Carrying Code, Santa Barbara, CA, 29 June 2000.
04. Hongwei Xi, A Dependently Typed Assembly Language,
ROPAS group, Department of Computer Science, Korea Advanced
Institute of Science and Technology (KAIST), Taejon, Korea,
7 April 1999.
03. Hongwei Xi, Dependent Types in Practical Programming,
ROPAS group, Department of Computer Science, Korea Advanced
Institute of Science and Technology (KAIST), Taejon, Korea,
6 April 1999.
02. Hongwei Xi, Dependenly Typed Assembly Language, Workshop on
Dependent Types in Programming, Goteborg, Sweden,
27 - 28 March 1999.
01. Hongwei Xi, Dependent Types in Practical Programming, Formal
Methods PI meeting, Stanford University, October 1998.
- * - * - * - * - * - * ------------------------------------------
Individual Student Guidance:
01. Songtao Xia, PhD student, Oregon Graduate Institute of
Science and Technology, August 1998 - August 1999.
02. Varun Nayak, MS student, University of Cincinnati,
January 2000 - May 2002. (Varun successfully defended his
Master's thesis in May 2002 and is now working for a company
in London, England)
03. Zaiwei Du, MS student, University of Cincinnati,
September 2000 - June 2001.
04. Sudeep Sabnis, MS student, University of Cincinnati,
January 2001 - August 2003. (Sudeep successfully defended
his Master's thesis in August 2003)
05. Dengping Zhu, PhD student, Boston University,
September 2001 - Present.
06. Chiyan Chen, PhD student, Boston University,
June 2002 - Present.
07. Sa Cui, PhD student, Boston University,
September 2002 - Present.
08. Rui Shi, PhD student, Boston University,
September 2002 - Present
- * - * - * - * - * - * ------------------------------------------
References:
Frank Pfenning (thesis advisor) James Hook (postdoc superviser)
Senior Research Computer Scientist Associate Professor and Director
Department of Computer Science Pacific Software Research Center
Carnegie Mellon University Department of Computer Sci & Eng
5000 Forbes Avenue Oregon Graduate Institute
Pittsburgh, PA 15213 P. O. Box 91000
Phone: +1 412 268-6343 Portland, OR 97291
Fax: +1 412 268-5576 Fax: + 1 503 1548
Email: fp+@cs.cmu.edu Email: hook@cse.ogi.edu
Robert Harper Peter Andrews
Associate Professor Professor
Department of Computer Science Department of Mathematical Sciences
Carnegie Mellon University Carnegie Mellon University
5000 Forbes Avenue 5000 Forbes Avenue
Pittsburgh, PA 15213 Pittsburgh, PA 15213
Phone: +1 412 268-3675 Phone: +1 412 268-2554
Fax: +1 412 268-5576 Fax: +1 412 268-5576
Email: rwh+@cs.cmu.edu Email: Peter.Andrews@cmu.edu
Russel Walker(teaching reference)
Senior Lecturer and Assistant Head
Department of Mathematical Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213
Phone: +1 412 268-2545
Fax: +1 412 268-5576
Email: Russell.Walker@cmu.edu
- * - * - * - * - * - * ------------------------------------------
Other information:
Membership ACM, AMS, IEEE
Languages Fluent in Chinese and English
- * - * - * - * - * - * ------------------------------------------