Hongwei Xi
Projects

ATS: A Language to Support Practical Programming with Theorem Proving

The immense complexity involved in software design and implementation is evident. In this day and age, software design is often expressed in forms of varying degree of formalism, ranging from verbal discussions to pencil/paper drawings to plain text descriptions to UML diagrams to specifications in languages such as Z, etc. Also, there is often an enormous gap between the design of a software system and its actual implementation, making it exceedingly difficult to construct software that meets its specification.

However, the very ability to construct software that meets its specification is crucial to (highly) dependable computing, and there seem to be no other shortcuts. We propose to design and implement a full-fledged programming language ATS with its type system rooted in the framework Applied Type System so that we can use types to formally capture (certain) specifications in software design and then resort to type-checking to enforce that the captured specifications be met in an actual implementation. In stark contrast to pure theorem proving systems where programs are extracted from proofs (instead of being constructed directly), ATS is to be designed as an effectful programming language that contains a pure theorem-proving subsystem to support the paradigm of programming with theorem proving. There is no program extraction in ATS. Instead, programs are constructed directly in ATS (while proofs in programs are to be erased before run-time to support efficient execution). We plan to evaluate the effectiveness of ATS in the construction of real and complex software systems.

Realistic Program Termination Verification: Theory and Practice

We propose to design a practical approach to program termination verification on realistic programs that includes both theoretical study and actual implementation. It is well-known that program termination verification is a challenging research subject of significant practical importance. In practice, the programmer often knows for some reasons that a particular program should terminate if implemented correctly. This immediately implies that a termination checker can be of great value for detecting program errors that cause nonterminating program execution. Unfortunately, termination checking in a realistic programming language that supports general recursion is often prohibitively expensive given that (a) program termination in such a language is in general undecidable, (b) termination checking often requires interactive theorem proving that can be too involved for the programmer, (c) a minor change in a program can often demand a renewed effort in termination checking and (d) a large number of changes are likely to be made in a program development cycle. In order to design a termination checker for practical use, these issues must be properly addressed.

In particular, we propose to design a novel type system that allows the programmer to supply metrics through dependent types for verifying program termination and prove that every well-typed program in this type system is terminating. We can thus turn termination verification into type-checking. However, it should be emphasized that we are not here advocating the design of a programming language in which only terminating programs can be written. Instead, we are interested in designing a mechanism in a programming language, which, if the programmer chooses to use it, can facilitate program termination verification. Striving for practicality, we intend to form such a mechanism that is both applicable to a large variety of realistic programs and unobtrusive to common programming styles. The major goals of the proposed research include

• designing a type system capable of guaranteeing programming termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic datatypes, polymorphism and effects, and
• establishing the soundness of the type system, that is, proving every well-typed program in this type system is terminating, and
• implementing a type-checker for the type system and providing realistic examples (in both functional and imperative programming) to assess the applicability of such a type system to realistic programming.

Xanadu: Imerative Programming with Dependent Types

We propose to enrich practical imperative programming with a type discipline that allows for specification and inference of significantly more precise information on programs than those enforced in languages such as Java and Standard ML (SML).

The primary motivation for developing such a type discipline is to enable the programmer to express more program properties with types and then enforce these properties through type-checking. It is well-known that a type discipline such as the one enforced in Java or SML can effectively facilitate program error detection. Therefore, it can be expected that a stronger type discipline can help detect more program errors, leading to the production of more robust software.

In general, there are two directions for extending a Hindley-Milner style of type system such as the one in SML. One is to extend it so that more programs can be admitted as type-correct and the other is to extend it so that programs can be assigned more accurate types. We are primarily interested in the latter.

The notion of dependent types, which was largely invented for modeling programs with more accuracy, has been studied for at least three decades. However, the use of dependent types in practical programming has been rare if there is any, and this, we think, is mainly caused by some great difficulty in designing a practically useful type inference algorithm for a dependent type system. We have presented an approach to addressing the difficulty in the design of Dependent ML (DML), which extends ML with a notion of restricted form of dependent types. It is also demonstrated that dependent types in DML can facilitate array bound check elimination, redundant pattern matching clause removal, tag check elimination and tagless representation of datatypes. Evidently, an immediate question is whether we can reap some similar benefits by incorporating dependent types into imperative programming. We propose to address this question by designing a dependently typed imperative programming language.

There is yet another motivation for incorporating dependent types into practical programming. In an untrusted computing environment such as Internet, mobile code received from an unknown source may not be trusted. Therefore, code recipient often needs to perform certain static and/or dynamic checks on received mobile code to prevent from happening some undesirable consequences such as security breach. We have designed a dependently typed assembly language (DTAL) in which the type system can guarantee the memory safety of DTAL code, where memory safety consists of both type safety and safe array subscripting. It is, however, difficult to compile into DTAL code a program written in a language such as Java since it often seems ineffective to synthesize from such a program the type information needed in DTAL code. With a dependently typed imperative programming language, we expect to implement a compiler that can translate dependent types at source level into dependent types at assembly level, effectively producing DTAL code.

In short, we propose to design a dependently typed imperative programming language for studying the use of dependent types in practical imperative programming at both source level and assembly level. We expect this study can eventually lead to the production of software that is not only more robust but also less costly to maintain.

Dependent Types for High-Confidence Distributed Systems

We propose to enrich distributed programming with a new type discipline. This discipline permits the specification and inference of significantly more precise information about distributed programs than is possible in current languages and notations (e.g., Java, CORBA, MPI). At the same time, this new discipline is only a small extension of the current practice in strongly-typed languages (e.g., those listed above).

The primary motivations for developing such a type discipline are: (i) to enable programmers to express an important class of program properties for distributed systems---liveness properties, and (ii) to enforce these properties through static and/or dynamic type-checking. It is well-known that a type discipline (such as the one enforced in Java) can be of great help for facilitating program error detection. Therefore, it is reasonable to believe that an extended type discipline could help detect program errors related to liveness, leading to the construction of more robust distributed software.

Liveness requirements are commonly expressed as global properties of an entire distributed system. This view, however, complicates reasoning about such requirements at the constituent component level. We have explored a collection of local properties, termed certificates, including properties for expressing liveness. We have developed a specification language using certificates and built a tool for supporting the testing of distributed components based on this specification language. To date, however, this post-hoc testing is the only practical means available to increase one's confidence in the correctness of code with respect to certificate specifications. Type systems, and in particular dependent types, offer a promising solution to this short-coming.

The notion of dependent types, which was largely invented for modeling programs with more accuracy, has been studied for at least three decades. However, the use of dependent types in practical programming has been rare if there is any, and this, we think, is mainly caused by some great difficulty in designing a practically useful type inference algorithm for a dependent type system. We have presented an approach to addressing the difficulty in the design of Xanadu, which extends imperative programming with a notion of restricted form of dependent types. It is demonstrated that dependent types in Xanadu can greatly facilitate the construction of memory safe programs, reducing the likelihood of abnormal program behavior caused by astray memory access and thus enhancing program robustness.

The use of dependent types in Xanadu so far is to ensure safety properties of programs. In this proposed research, we intend to demonstrate that dependent types can also be used to ensure liveness properties of programs. In particular, we will study the use of dependent types in establishing program termination, which is often the key to establishing many other liveness properties.

The major goals of this proposed research are to:

• Design a dependent type system that is capable of handling program termination in practice and establishing its soundness.
• Implement a type-checker for this dependent type system to demonstrate its use in constructing distributed programs.
• Ensure that the new type discipline is no more onerous than ordinary types, with extra effort required only if higher confidence is needed.
• Provide realistic examples to assess the benefits of dependent types in distributed computing.

[ Home | Contact | CV | Research | Publications ]
[ Projects | Courses ]
[ UC Flying Club | UC Skydiving Club ]

hwxi AT cs DOT bu DOT edu
http://www.cs.bu.edu/~hwxi