|
The Fox Project
|
| Contents | Recent Talks | Recent Publications | Software | Collaborations | Further Links |
|---|---|
| Elsewhere | Bibliography |
Typed intermediate languages extend the benefits of type safety enjoyed by high-level source programming languages to the intermediate and target languages of a compiler. This is achieved by a generalization of syntax-directed compilation, called type-directed compilation. In a type-directed compiler, source code is translated into object code, and, at the same time, the type of the source code is translated into a type of the object code. The translation of the source code is guaranteed to have as its type the translation of the source type, so that well-typed programs at the source level are translated into well-typed programs at the object level.
Since well-typed source programs enjoy strong safety properties, so also do the corresponding target programs. By type checking the target code we can assure ourselves of its safety without having to trust the correctness of the compiler. A compiler that generates typed object code is an example of a certifying compiler whose object code can be mechanically checked for safety by any user of its generated code. Certifying compilers therefore provide a foundation for trust-free code dissemination in which code can be shared in an untrusted environment without sacrificing safety. By type checking intermediate code during compilation, we may build a self-checking compiler that verifies its own integrity by type checking the intermediate code produced by each compiler transformation. This greatly enhances the reliability of the compiler and greatly facilitates team development.
Type-directed certifying compilers support heterogenous component integration. Since typed object code comes equipped with types, we may rely on its safety without assuming that it arises from any one compiler or any one language. The same typed object code may arise from several different compilers for several different (type-safe) languages. This type information may then be used to mediate component integration to ensure the safety of composite systems. A type-safe linker can ensure that the typing requirements of individual components are satisfied when they are linked, either statically or dynamically, in a running system.
Type-directed compilers support the generation of efficient object code. Most existing compilers make serious compromises of efficiency in order to support automatic storage management or to permit the decomposition of programs into independent modules or components. By exploiting type information during compilation and at execution time, a type-directed compiler can avoid these compromises while preserving the benefits of storage management and modularity.
The Fox Project pioneered the development of type-directed compilers. The project is currently investigating both the foundations of type-directed compilation, such as the design of type systems for intermediate and object code, and the engineering problems of implementing type-directed compilers for full-scale programming languages. Our current research artifact is the TILT compiler (Typed Intermediate Languages, Two) for Standard ML.
Overview references:
[ Home
| Contact Information
| Publications
| Researchers
]
[ FoxNet
| Typed Intermediate Languages
| Proof-Carrying Code
]
[ Logical Frameworks
| Staged Computation
| Language Design
]