What Are Polymorphically-Typed Ambients?
| Autor: | Torben Amtoft, Assaf Kfoury, Santiago M. Pericás-Geertsen |
|---|---|
| Rok vydání: | 2001 |
| Předmět: |
Computer science
Process calculus Semantics computer.software_genre Lambda cube Operational semantics Denotational semantics Ambient calculus Calculus of communicating systems Discrete mathematics Finite-state machine Simply typed lambda calculus Type inhabitation Natural deduction Programming language System F Decidability Pure type system TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Conservative extension TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Subject reduction Automata theory Typed lambda calculus computer Normalisation by evaluation |
| Zdroj: | Programming Languages and Systems ISBN: 9783540418627 ESOP |
| Popis: | 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]. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|