%0 Journal Article
%T Standard Type Soundness for Agents and Artifacts
%A F. Damiani
%A P. Giannini
%A A. Ricci
%A M. Viroli
%J Scientific Annals of Computer Science
%D 2012
%I Alexandru Ioan Cuza University of Iasi
%X Formal models, core calculi, and type systems, are important tools for rigorously stating the more subtle details of a language, to characterise and study its features and the correctness properties of its programs. In this paper we present {FsimpAL} (FsimpaALlong), a formal calculus modelling the agent and artifact program abstractions provided by the simpA{} agent framework. The formalisation is largely inspired by extsc{Featherweight Java}. It is based on reduction rules applied at 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 {FsimpAL} distinctive primitives.
%K multi-agent systems
%K concurrency
%K type systems
%U http://www.infoiasi.ro/bin/download/Annals/XXII2/XXII2_1.pdf