Standard type soundness for agents and artifacts

Ferruccio Damiani, Paola Giannini, Alessandro Ricci, Mirko Viroli

Risultato della ricerca: Contributo su rivistaArticolo in rivistapeer review

Abstract

Formal models, core calculi, and type systems, are important tools for rigorously stating the more subtle details of a language, as well as characterizing and studying its features and the correctness properties of its programs. In this paper we present FAAL (Featherweight Agent and Artifact Language), a formal calculus modelling the agent and artifact program abstractions provided by the simpA agent framework. The formalisation is largely inspired by Featherweight Java. It is based on reduction rules applied in certain evaluation contexts, properly adapted to the concurrency nature of simpA. On top of this calculus we introduce a standard type system and prove its soundness, so as to guarantee that the execution of a well-typed program does not get stuck. Namely, all primitive mechanisms of agents (activity execution), artifacts (field/property access and step execution), and their interaction (observation and invocation) are guaranteed to be used in a way that is structurally compliant with the corresponding definitions: hence, there will not be run-time errors due to FAAL distinctive primitives.

Lingua originaleInglese
pagine (da-a)267-326
Numero di pagine60
RivistaScientific Annals of Computer Science
Volume22
Numero di pubblicazione2
DOI
Stato di pubblicazionePubblicato - 2012

Fingerprint

Entra nei temi di ricerca di 'Standard type soundness for agents and artifacts'. Insieme formano una fingerprint unica.

Cita questo