Handling Mobility Failures by Modal Types

Correctness is a major concern for logical systems, especially for its significance in computational settings. While establishing a norm for the correctness of computational procedures is a standard requirement, defining errors is a less investigated formal problem. In typed systems, in particular, errors are dealt with by rising execeptions and when their resolution fails, these are followed by abortion procedures. In distributed systems, this corresponds to error detection and service restart. More efficient error resolution strategies for code mobility failures in distributed computing can be defined by re-evaluation and re-addressing of resources in referentially transparent expressions. We formulate a substructural modal type system to analyse failure of mobile code and appropriate resolution strategies when abortion is not required. We provide local soundness and completeness results, analyse restricted structural properties, show reduction and expansion on failure states and offer a simple application of the language. Moreover, we design a state transition semantics and offer soundness and completeness results with respect to the proof theory.