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.
Settore PHIL-02/A - Logica e filosofia della scienza
   BIAS, RISK, OPACITY in AI: design, verification and development of Trustworthy AI
   BRIO
   MINISTERO DELL'ISTRUZIONE E DEL MERITO
   2020SSKZ7R_001

   Dipartimenti di Eccellenza 2018-2022 - Dipartimento di FILOSOFIA
   MINISTERO DELL'ISTRUZIONE E DEL MERITO
2-ott-2024
Book Part (author)
File in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/1106148
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact