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:

Alice and Bob ate 10 apples together. Alice ate 3 apples. What is the number of apples eaten by Bob? 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:
  • Let A and B stand for the numbers of apples eaten by Alice and Bob, respectively.
  • A+B=10
  • A=3
  • What is the value of B?
  • 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 programming 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