Intuitionistic Modal Logic and Applications Workshop (IMLA11), Nancy

TitleA multi-modal type system and its procedural semantics for safe distributed programming
Publication TypeTechnical Report
Year of Publication2011
AuthorsPrimiero, G
Series TitleIntuitionistic Modal Logic and Applications Workshop (IMLA11), Nancy

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.

Citation Keyprimiero2011multi
Download PDF (Author PDF)
PDF author (public):