|Principal Investigator||Hongwei Xi|
|Support||NSF CCF-1018601, 2010 - 2013|
|Keywords||ATS, Systems Programming, Applied Type System, Linear Types, Dependent Types|
Typical system design is marked by tradeoffs between factors such as efficiency and reliability, features and security, etc. As of now, most low-level systems (e.g, operating systems) are written in unsafe programming languages that are either untyped (e.g., assembly) or weakly typed (e.g., C). Evidently, a question of great interest is why people (in general) do not implement these systems in existing safe languages such as Java. Among a variety of reasons, a particularly important one is that low-level features such as explicit use of pointers and pointer arithmetic are disallowed in such safe languages in order to guarantee safety. However, the very need to achieve optimal hardware usage often demands the availability of such features. In addition, the requirement for run-time garbage collection (GC) by safe languages can often become a great or even insurmountable obstacle when handling of real-time events must meet hard deadlines. Can we have a safe and practical programming language that also supports low-level programming features?
ATS is a full-fledged programming language with a type system rooted in the framework Applied Type System. ATS can run without GC and it supports low-level features such as pointers and pointer arithmetic. When such features are used, the programmer is required to construct proofs within ATS to justify the safety of their use. This is a programming paradigm we refer to as programming with theorem-proving. In this project, we are to investigate approaches that allow ATS to be effectively employed in the construction of safe and reliable low-level systems. In particular, we are to make extensive use of programming with theorem-proving in the design and implementation of kernel data structures so as to guarantee their being implemented as well as used correctly. We are also to rely on dependent types and linear types to track the manipulation of computing resources, preventing potential misuses. At the minimum, we are to build a running OS in ATS to demonstrate the practicality of combining systems programming with theorem-proving. However, the goal of the project is not about implementing a particular "one-off" OS in ATS. Instead, we aim to identify and then formalize approaches that can greatly enhance the quality of low-level systems design and implementation by making use of advanced type theory.
|Principal Investigator||Hongwei Xi|
|Support||NSF CCF-0702665, 2007 - 2010|
|Keywords||ATS, Applied Type System, Dependent Types|
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.
|Principal Investigator||Hongwei Xi|
|Support||NSF CCR-0092703 (CAREER Award), 2001 - 2006|
|Keywords||Program Termination, Dependent Types, DML|
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
|Principal Investigator||Hongwei Xi|
|Support||NSF ITR-0081316, 2000 - 2003|
|Keywords||Dependent Types, Xanadu, DTAL|
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.
|Principal Investigators||Paul Sivilotti and Hongwei Xi|
|Support||Ohio Board of Regents, 2000 - 2002|
|Keywords||Dependent Types, Transience, Termination, Liveness|
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: