Flow-sensitive type systems and the ambient calculus Export

@article{citeulike:3610906, abstract = {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).}, author = {Amtoft, Torben}, citeulike-article-id = {3610906}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1466791}, citeulike-linkout-1 = {http://dx.doi.org/10.1007/s10990-008-9039-z}, citeulike-linkout-2 = {http://www.springerlink.com/content/882q503g28403w86}, doi = {10.1007/s10990-008-9039-z}, journal = {Higher-Order and Symbolic Computation}, keywords = {ambient, flowtype}, posted-at = {2009-05-05 04:37:55}, priority = {2}, title = {Flow-sensitive type systems and the ambient calculus}, url = {http://dx.doi.org/10.1007/s10990-008-9039-z} }

TY - JOUR ID - citeulike:3610906 L3 - citeulike-article-id:3610906 N2 - 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). JF - Higher-Order and Symbolic Computation TI - Flow-sensitive type systems and the ambient calculus KW - ambient KW - flowtype AU - Amtoft, Torben UR - http://dx.doi.org/10.1007/s10990-008-9039-z ER -