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