What Are Polymorphically-Typed Ambients?

The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code [CG98]. 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. Our polymorphically-typed calculus is a conservative extension of the typed Ambient Calculus originally proposed by Cardelli and Gordon [CG99].

• Type: Conference
• Year: 2001
• Where: ESOP
• Authors: Torben Amtoft, A. J. Kfoury, Santiago M. Pericás-Geertsen
• Keywords: Ambient Calculus, Cardelli, ESOP 2001, Polymorphically-typed Calculus, Programming Languages