Flow-sensitive type systems and the ambient calculus |
| |
Authors: | Torben Amtoft |
| |
Affiliation: | (1) Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506, USA |
| |
Abstract: | The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code.
Numerous analyses have been developed for numerous variants of that calculus. We take up the challenge of developing, in a
type-based setting, a relatively precise “topology” analysis for the original version of the calculus. To compensate for the lack of “co-capabilities” (an otherwise increasingly popular extension), the
analysis is flow-sensitive, with the actions of processes being summarized by “behaviors”.
A subject reduction property guarantees that for a well-typed process, the location of any ambient is included in what is
predicted by its type; additionally it ensures that communicating subprocesses agree on their “topic of conversation”. Based
on techniques borrowed from finite automata theory, type checking of type-annotated processes is decidable (though potentially
exponential). |
| |
Keywords: | Ambient calculus Program analysis Type system Effect system Flow-sensitive analysis Behavior of mobile processes |
本文献已被 SpringerLink 等数据库收录! |
|