Nomadic π-calculi: expressing and verifying communication infrastructure for mobile computation

摘要: Abstract This thesis addresses the problem of verifying distributed infrastructure for mobile computa-tion. In particular, we study language primitives communication between agents.They can be classified into two groups. At a low level there are location dependent primitivesthat require programmer to know current site agent in order communicatewith it. high independent that allow communicationwith irrespective any migrations. Implementation requiresdelicate algorithms. earlier work Sewell, Wojciechowski andPierce, levels were made precise as process calculi, allowing such algorithms ex-pressed encodings level; programming languageNomadic Pict has been built experimenting with encodings.This turns semantics, giving definition core (with type system)and proving correctness an example infrastructure. involves extending standardsemantics and proof techniques calculi deal new notions sites andagents. The adopted include labelled transition operational equiv-alences preorders (eg. expansion coupled simulation), “up to” equivalences, anduniform receptiveness. We also develop novel capturing designintuitions regarding agents: consider translocating versions take migration account, compositional reasoning; temporaryimmobility, which captures intuition while is waiting lock somewherein system, it will not migrate.The non-trivial. It analysing thepossible reachable states encoding applied arbitrary high-level source program.We introduce intermediate factoring out many ‘house-keeping’ reductionsteps possible, focusing on partially-committed steps.iii