| |
 |
Welcome! |
 |
| 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) |
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 StudentsI 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
|