Title: What are polymorphically-typed ambients?
Authors: Torben Amtoft, Assaf Kfoury, Santiago Pericas-Geertsen
Date: October 19, 2000
Abstract: The Ambient Calculus was developed by Cardelli and
Gordon as a formal framework to study issues of mobility and
migrant code. We consider an Ambient Calculus where ambients
transport and exchange programs rather that just inert data. We
propose different senses in which such a calculus can be said to be
polymorphically typed, and design accordingly a polymorphic
type system for it. Our type system assigns types to embedded
programs and what we call behaviors to processes; a denotational
semantics of behaviors is then proposed, here called trace
semantics, underlying much of the remaining analysis. We state
and prove a Subject Reduction property for our polymorphically
typed calculus. Based on techniques borrowed from finite automata
theory, type-checking of fully type-annotated processes is shown
to be decidable; the time complexity of our decision procedure is
exponential (this is a worst-case in theory, arguably not encountered
in practice). Our polymorphically-typed calculus is a conservative
extension of the typed Ambient Calculus originally proposed by
Cardelli and Gordon.