Spatial and Behavioral Types in the Pi-Calculus

Autor:	Lucia Acciai, Michele Boreale
Rok vydání:	2008
Předmět:	TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Theoretical computer science Spatial model Pi calculus Process (engineering) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Liveness Declaration Class (philosophy) Type (model theory) Algorithm Scope (computer science) Mathematics
Zdroj:	CONCUR 2008-Concurrency Theory ISBN: 9783540853602 CONCUR
DOI:	10.1007/978-3-540-85361-9_30
Popis:	We present a framework that combines ideas from spatial logics and Igarashi and Kobayashi's behavioural type systems, drawing benefits from both. In our approach, type systems for the pi-calculus are introduced where newly declared (restricted) names are annotated with spatial process properties, predicating on those names, that are expected to hold in the scope of the declaration. Types are akin to ccs terms and account for the processes abstract behaviour and "shallow" spatial structure. The type systems relies on spatial model checking, but properties are checked against types rather than against processes. The considered class of properties is rather general and, differently from previous proposals, includes both safety and liveness ones, and is not limited to invariants.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::1be124c57c6b829ecc6453bc7694844b https://doi.org/10.1007/978-3-540-85361-9_30 Zobrazit plný text záznamu