Type and E ect Systems - Correct System Design: Recent Insights and Advances - page 109

Type and Eect Systems

Flemming Nielson and Hanne Riis Nielson

Department of Computer Science, Aarhus University, Denmark.

Abstract. The design and implementation of a correct system can ben-
et from employing static techniques for ensuring that the dynamic be-
haviour satises the specication. Many programming languages incor-
porate types for ensuring that certain operations are only applied to data
of the appropriate form. A natural extension of type checking techniques
is to enrich the types with annotations and eects that further describe
intensional aspects of the dynamic behaviour.

Keywords. Polymorphic type systems, eect annotations, subeecting
and subtyping, semantic correctness, type inference algorithms, syntac-
tic soundness and completeness. Analyses for control flow, binding times,
side eects, region structure, and communication structure.

1 Introduction

Static analysis of programs comprises a broad collection of techniques for pre-
dicting safe and computable approximations to the set of values or behaviours
arising dynamically during computation; this may be used to validate program
transformations, to generate more ecient code or to increase the understanding
of the software so as to demonstrate that the software satises its specication.
We shall nd it helpful to divide the techniques into the following two approaches.
The flow based approach includes the traditional data flow analysis techniques
for mainly imperative and object-oriented languages; it also includes the con-
straint based control flow analysis techniques developed for functional and object
oriented languages; nally, it includes the use of mathematical modelling in the
abstract interpretation of imperative, functional, concurrent and logic languages.
The inference based approach includes general logical techniques touching upon
program verication and model checking; it also includes type and eect sys-
tems developed for functional, imperative and concurrent languages and it is
this latter group of techniques that we consider here.
We shall suppose that a typed programming language is given. In soft typing
all programs can be typed because a \top" type can be used in the absence
of meaningful \ordinary" types; this perspective is similar to that of the flow
based approach and is quite useful for analysing the behaviour of programs but
is less useful for enforcing the absence of dynamic errors. In this paper we focus
on strong typing where no \top" type is around and where certain erroneous