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
ATS : A Language to Support Practical Programming with Theorem Proving
Current Courses None
Conferences The 2008 ACM SIGPLAN Workshop on ML, Victoria, British Columbia, Canada, September 21st, 2008
(PC member)
The 3rd workshop on Logic and Semantic Frameworks, with Applications (LSFA'08), San Salvador, Brazil, August 26th, 2008
(PC member)

BU CS Graduate Program

BU CS PL Reading Group

Recent Drafts and Publications

  • Hongwei Xi, ATS/LF: a type system for constructing proofs as total functional programs. In the Festschrift in honor of Peter Andrews on the occasion of his 70th birthday, Studies in Logic and Foundations of Mathematical Logic, February 2008. (pdf) (ps)

  • Hongwei Xi, Attributive Types for Proof Erasure. In the post-workshop proceedings of the international workshop TYPES'07, LNCS vol. 4941, December 2007. (pdf) (ps)

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


    Research Students

    I am currently working with the following student(s):

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

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