TY - RPRT T1 - A multi-modal type system and its procedural semantics for safe distributed programming Y1 - 2011 A1 - Primiero, Giuseppe AB -

In this paper we present a multi-modal polymorphic type system for a computational interpretation of programs with distributed resources. Polymorphism induces a distinction between programs whose code is safe at location, and programs whose value is safe overall. We formulate judge- mental modalities to express such distinction and use their introduction and elimination rules to express mobility of code and values within a net- work. The syntactic formulation is completed by a procedural semantics interpreted over states of an abstract machine for which a standard sound- ness result is given in the form of a type safety theorem.

JA - Intuitionistic Modal Logic and Applications Workshop (IMLA11), Nancy ER -