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 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 - * - * - * - * - * - * ------------------------------------------