This paper presents a lter model for -calculus and shows its full abstraction with respect to a `may' operational semantics. The model is introduced in the form of a type assignment system. Types are related by a preorder that mimics the operational behaviour of terms. A subject expansion theorem holds. Terms are interpreted as lters of types: this interpretation is compositional. The proof of full abstraction relies on a notion of realizability of types and on the construction of terms, which test when an arbitrary term has a xed type.
Titolo: | A Filter Model for Mobile Processes | |
Autori Riconosciuti: | ||
Autori: | DAMIANI F.; M. DEZANI; GIANNINI P. | |
Data di pubblicazione: | 1999 | |
Abstract: | This paper presents a lter model for -calculus and shows its full abstraction with respect to a `may' operational semantics. The model is introduced in the form of a type assignment system. Types are related by a preorder that mimics the operational behaviour of terms. A subject expansion theorem holds. Terms are interpreted as lters of types: this interpretation is compositional. The proof of full abstraction relies on a notion of realizability of types and on the construction of terms, which test when an arbitrary term has a xed type. | |
Volume: | 9(1) | |
Pagina iniziale: | 63 | |
Pagina finale: | 102 | |
Digital Object Identifier (DOI): | 10.1017/S096012959800259X | |
URL: | http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=44771 | |
Rivista: | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE | |
Appare nelle tipologie: | 03A-Articolo su Rivista |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.