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]

   
 
Welcome!

Hongwei Xi picture

Assistant Professor   Curriculum Vitæ(pdf)(ps)
hwxi AT cs DOT bu DOT edu   Publications
     
Computer Science Department   Office:   172 MCS Building
Boston University   Phone:   +1 617 358 2511
111 Cummington Street, Boston, MA 02215, U.S.A.   Fax:   +1 617 353 6457
 
Research Interests Programming Languages, Type Theory, Theorem Proving
Compiler Optimization, Software Engineering
Ph.D. Thesis Dependent Types in Practical Programming
(ps) (ps gzipped) (pdf) (pdf gzipped)
Projects
Church The development of computer software satisfying well-defined formal criteria of efficiency, reliability and safety
ATS Applied Type System
Xanadu Imperative Programming with Dependent Types
DML Dependent ML
Current Courses BU CAS CS 320  Concepts of Programming Languages, Fall 2006, TR 11AM-12:30PM, MCS B33
Conferences ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), Tucson, AZ, June, 2008
(PC member)
The 2nd workshop on Programming Languages meet Program Verification (PLPV'07), Freiberg, Germany, October 5th, 2007
(Co-Chair with Aaron Stump)
The 2nd workshop on Logic and Semantic Frameworks, with Applications (LFSA'07), Ouro Preto, Brazil, August 28th, 2007
(PC member)

BU CS Graduate Program

BU CS PL Reading Group

Recent Drafts and Publications

  • 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)

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

  • Kevin Donnelly and Hongwei Xi, A Formalization of Strong Normalization for Simply Typed Lambda-Calculus and System F. In Proceedings of Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Seattle, WA, August 2006. (bibtex) (pdf) (ps) (code for stlc) (code for system f) (slides in ps) (slides in pdf)

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

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

  • 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), LNAI vol. 3717, pp. 310-320, Vienna, Austria, September 2005. (bibtex) (pdf) (ps)


    Research Students

    I am currently working with the following students:

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

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