Hongwei Xi
Research Interests
How many times have you heard someone saying "I know the answer but I can't
explain it"? A lot, I bet. I can easily tell the image of a cat from that
of a dog, but I cannot explain how I do it. In programming, it is often
easier for someone to write code than to explain what the code actually
does. This is very worrisome, especially, if we want to build high-quality
software systems.
In order to be precise, we need to be able to state clearly what we want.
Let me use the following elementary problem as an example:
My daughter, a first grader, had no difficulty telling me immediately that
the answer is 7. I, however, wanted her to give me a more formal
specification of the problem. We essentially came up with the following one
at the end:
With this specification, we could readily and formally derive that (A+B)-A
= 10-3. Addition being both commutative and associative, we derived
(A+B)-A = B+0 = B. Therefore, B = 7. So we not only found that 7 is an
answer but also proved that 7 is the unique answer.
While I might have been a bit overly pedantic about the above elementary
problem, I do hope that you can see my point of being precise here. I
strive to be precise in programming and have a passion
for effectively enforcing precision in realistic software
development.
Academically, 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 continuing 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 have already been incorprated
into ATS, which include:
- Functional programming.
While ATS is primarily a language based on eager call-by-value evaluation,
it also supports lazy, that is, call-by-need evaluation.
- Imperative programming (with safe support for explicit pointers and
pointer arithmetic)
- 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 demonstrate 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
|