Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Properties of a Type Abstract Interpreter
| |
|
Properties of a Type Abstract Interpreter
Roberta Gori8 and Giorgio Levi8 
| (8) |
Dipartimento di Informatica, Università di Pisa, Pisa, Italy |
Abstract
In a previous paper [7], we have developed a type abstract interpreter which was shown to be more precise then the classical ML type inference algorithm
in inferring monomorphic types, represented as Herbrand terms with variables à la Hindley. In order to deal with recursive
functions, we introduce a new abstract fixpoint operator which generalizes the one used in the Hindley and ML inference algorithms
by performing k fixpoint computation steps (as done in [11] in the case of polymorphic types). Our abstract interpreter has many interesting properties. It is possible to reconstruct
the ML result by just one fixpoint computation step (k = 1) and to show that for every k ≥ 1, either we reach the least fixpoint (which is in general more precise than the ML result), or we get exactly the same
result as ML. One important result is that our type interpreter turns out to correspond to a type system, which lies between
monomorphism and polymorphic recursion.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|