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.
Handling Mobility Failures by Modal Types / G. Primiero (LOGIC, EPISTEMOLOGY, AND THE UNITY OF SCIENCE). - In: The Architecture and Archaeology of Modern Logic / [a cura di] A. Klev. - Cham : Springer Nature, 2024 Oct 02. - ISBN 9783031524103. - pp. 203-232 [10.1007/978-3-031-52411-0_11]
Handling Mobility Failures by Modal Types
G. Primiero
2024
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
978-3-031-52411-0_11.pdf
accesso riservato
Descrizione: Book Chapter
Tipologia:
Publisher's version/PDF
Dimensione
691.09 kB
Formato
Adobe PDF
|
691.09 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.