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

ence algorithm. Formulations of syntactic soundness are mostly rather straight-
forward: the result produced by the algorithm must give rise to a valid inference
in the inference system. A simple example is the following: if

W ( Γ; e )=( S; ; ' )

then must hold; here it is clear that the substitution produced

is intended to rene the initial information available when rst calling the al-
gorithm. A somewhat more complex example is: if

S ( Γ ) ` e : & '

W ( Γ; e )=( S; ; '; C )then

S 0 ( S 0 ( S 0 ( S 0 is a solution to the con- S ( Γ )) ` e : )& ' ) must hold whenever

straints in C . The proofs are normally by structural induction on the syntax of

programs.

The formulations of syntactic completeness are somewhat more involved. Given
a program e such that Γ ` e : & ' , the main diculty is to show how this

can be obtained from ). The solution

is to formally dene when one \typing" is an instance of another; the notion of
lazy instance [9] is very useful here and in more complex scenarios Kripke-logical
relations (see e.g. [28]) may be needed [1]. The proofs are often challenging and
often require developing extensive techniques for \normalising" deductions made
in the inference system so as to control the use of non-syntax directed rules. For
suciently complex scenarios syntactic completeness may fail or may be open
(as mentioned above); luckily soundness often suces for the inference algorithm
to be of practical use.

W ( Γ; e )=( S; ; ' )or W ( Γ; e )=( S; ; '; C

Exploitation. Exploitation is a rather open-ended area although it would seem
that the integration of program analyses and program transformations into an
inference based formulation is quite promising [46]. Indeed, inference-based for-
mulations of analyses can be seen as an abstract counterpart of the use of at-
tribute grammars when developing analyses in compilers, and in the same way
inference-based formulations of analyses and transformations can be seen as an
abstract counterpart of the use of attributed transformation grammars [47].

6 Conclusion

The approach based on type and eect systems is a promising approach to the
static analysis of programs because the usefulness of types has already been
widely established. The main strength lies in the ability to interact with the
user: clarifying what the analysis is about (and when it may fail to be of any
help) and in propagating the results back to the user in an understable way
(which is not always possible for flow based approaches working on intermediate
representations). The main areas of further research concern the expressiveness
of the inference based specications, the complexity and decidability of the in-
ference algorithms and the interplay with the other approaches to static analysis
of programs.