Applied type system: Extended abstract

Abstract

The framework Pure Type System (PTS) offers a simple and general approach to designing and formalizing type systems. However, in the presence of dependent types, there often exist some acute problems that make it difficult for PTS to accommodate many common realistic programming features such as general recursion, recursive types, effects (e.g., exceptions, references, input/output), etc. In this paper, we propose a new framework Applied Type System (ATS) to allow for designing and formalizing type systems that can readily support common realistic programming features. The key salient feature of ATS lies in a complete separation between statics, in which types are formed and reasoned about, and dynamics, in which programs are constructed and evaluated. With this separation, it is no longer possible for a program to occur in a type as is otherwise allowed in PTS. We present not only a formal development of ATS but also mention some examples in support of using ATS as a framework to form type systems for practical programming. © Springer-Verlag 2004.