Name
Abstract | ||
|---|---|---|
The Ambient Calculus was developed by Cardelli and Gordon as a formal framework to study issues of mobility and migrant code [6]. 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 [7]. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-45309-1_14 | ESOP |
Keywords | Field | DocType |
different sense,ambient calculus,polymorphically-typed ambients,conservative extension,trace semantics,denotational semantics,polymorphically-typed calculus,subject reduction property,polymorphic type system,finite automata theory,type system,ambients transport,polymorphism,finite automata,technical report,automata theory | Discrete mathematics,Programming language,Normalisation by evaluation,Typed lambda calculus,Simply typed lambda calculus,Computer science,Lambda cube,System F,Pure type system,Ambient calculus,Process calculus | Conference |
Volume | ISSN | ISBN |
2028 | 0302-9743 | 3-540-41862-8 |
Citations | PageRank | References |
25 | 1.14 | 30 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Torben Amtoft | 1 | 364 | 29.25 |
| A. J. Kfoury | 2 | 461 | 47.34 |
| Santiago M. Pericás-Geertsen | 3 | 25 | 1.14 |