| |
 |
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 |
The 2nd workshop on
Programming Languages meet Program Verification (PLPV'07), Freiberg,
Germany, October, 2007
(Co-Chair with Aaron Stump) |
Hongwei Xi, Dependent ML: an approach to practical programming with
dependent types, September 2006. (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)
Hongwei Xi, Implmenting an evaluator for mini-ML in ATS: a case of programming with theorem proving.
Invited talk at the Fifth International Workshop on Reduction Strategies in
Rewriting and Programming (WRS'05), Nara, Japan,
April 22, 2005. (code) (pdf) (ps) (slides in ps)
Chiyan Chen,
Rui Shi and
Hongwei Xi, Implementing Typeful Program Transformations, Fundamenta Informaticae, vol. 69 (1-2),
pp. 103-121, 2005. (bibtex) (pdf) (ps)
Hongwei Xi and Dengping Zhu and
Yanka Li, Applied Type System with Stateful Views. Technical
Report, no. BUCS-2005-03, Computer Science Department, Boston University,
January, 2005. (pdf) (ps)
Chiyan Chen and
Hongwei Xi, Meta-Programming through Typeful Code Representation,
Journal of Functional
Programming, vol. 15(6), pp. 797-835, 2005. (bibtex) (pdf) (ps)
Dengping Zhu and
Hongwei Xi, Safe Programming with Pointers through Stateful Views.
In Proceedings of the 7th International Symposium on Practical Aspects of
Declarative Languages (PADL'05), LNCS vol. 3350, pp. 83--97, Long Beach,
CA, January 2005. (bibtex) (pdf) (ps)
(slides in ppt)
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
|