Static Type Systems: From Specification to Implementation

Abstract

Static type systems are fundamental tools used to determine properties of programs before execution. There exist several techniques for validation and verification of programs based on typing. Thus, type systems are important to know for the practicioner. When designing and implementing a technique based on typing systems, there is usually a gap between the formal tools used to specify it, and the actual implementations. This gap can be an obstacle for language designers and programmers. A better understanding of the features of a type system and how they are implemented can help enourmously to the good design and implementation of new and powerful verification methods based on type systems. This chapter addresses the problem of specifying and implementing a static type system for a simple language, but containing many of the subtleties found in bigger, mainstream languages. This contributes to the understanding of the techniques, thus bridging the gap between theory and practice. Additionally, the chapter contains a small survey of some of the existing developments in the static typing area and the static analysis based on typing.