Hongwei Xi
Research Interests
My primary research focuses on the design and implementation of programming
languages. I have also developed keen interests to promoting software
engineering benefits through programning language design. Ideally, a
programming language should be simple and general, and it should permit
extensive error checking, facilitate proofs of program properties and
possess a correct and efficient implementation. Invariably, there will be
conflicts among these goals, which must be resolved with careful attention
paid to the needs of the user. In order to make significant progress, I
firmly believe the necessity to adopt approaches that are capable of
addressing realistic problems.
Through many years of continued efforts, I, working with several graduate
students, have designed and implemented ATS, a programming language with
a highly expressive type system rooted in the framework Applied Type
System.
In particular, both dependent types and linear types are available in
ATS. Also, a variety of programming paradigms are already incorprated into
ATS, which include:
- Functional programming.
While ATS is primarily a language based on eager call-by-value evaluation,
it also supports lazy call-by-need evaluation.
- Imperative programming (with pointers)
- Object-oriented programming
- Concurrent programming (with pthreads)
- Modular programming.
The module system of ATS is largely infuenced by that of Modula-3, which is
both simple and general as well as effective in supporting large scale
programming.
In addition, ATS contains a component ATS/LF that supports a form of
(interactive) theorem proving, where proofs are written as total functions.
With this component, ATS advocates a programming style that combines
programming with theorem proving. Furthermore, ATS/LF can act as
a logical framework for encoding various deduction systems and their
(meta-)properties.
As of now, my primary research interest centers around implementing real
and complex systems in ATS that can convincingly demostrate the power of
advanced types such as dependent types and linear types in facilitating
the construction of high quality software.
[ Home
| Contact
| CV
| Research
| Publications
]
[ Projects
| Courses
]
hwxi AT cs DOT bu DOT edu
http://www.cs.bu.edu/~hwxi
|