@article {primiero2012modal, title = {A modal type theory for formalizing trusted communications}, journal = {Journal of Applied Logic}, volume = {10}, number = {1}, year = {2012}, pages = {92{\textendash}114}, abstract = {

This paper introduces a multi-modal polymorphic type theory to model epistemic processes characterized by trust, defined as a second-order relation affecting the communication process between sources and a receiver. In this language, a set of senders is expressed by a modal prioritized context, whereas the receiver is formulated in terms of a contextually derived modal judgement. Introduction and elimination rules for modalities are based on the polymorphism of terms in the language. This leads to a multi-modal non-homogeneous version of a type theory, in which we show the embedding of the modal operators into standard group knowledge operators.

}, doi = {10.1016/j.jal.2011.12.002}, author = {Primiero, Giuseppe and Taddeo, Mariarosaria} } @article {primiero2011multi, title = {A multi-modal type system and its procedural semantics for safe distributed programming}, year = {2011}, abstract = {

In this paper we present a multi-modal polymorphic type system for a computational interpretation of programs with distributed resources. Polymorphism induces a distinction between programs whose code is safe at location, and programs whose value is safe overall. We formulate judge- mental modalities to express such distinction and use their introduction and elimination rules to express mobility of code and values within a net- work. The syntactic formulation is completed by a procedural semantics interpreted over states of an abstract machine for which a standard sound- ness result is given in the form of a type safety theorem.

}, author = {Primiero, Giuseppe} } @conference {primiero2010multi, title = {A Multi-Modal Dependent Type Theory for Representing Data Accessibility in a Network.}, booktitle = {Electronic Proceedings of the Federated Logic Conference 2010 (Proof Systems for Program Logics Workshop)}, year = {2010}, publisher = {Citeseer}, organization = {Citeseer}, abstract = {

In this paper we present a multi-modal polymorphic constructive type theory for a computational interpretation of programs equipped with locations for data accessibility in the context of distributed processing.

}, author = {Primiero, Giuseppe} } @article {GiJ:mmac, title = {Majority Merging by Adaptive Counting}, journal = {Synthese (KRA Serie)}, volume = {165}, number = {2}, year = {2008}, pages = {203{\textendash}223}, abstract = {

The present paper introduces a belief merging procedure by majority using the standard format of Adaptive Logics. The core structure of the logic ADM(c) (Adaptive Doxastic Merging by Counting) consists in the formulation of the conflicts arising from the belief bases of the agents involved in the procedure. A strategy is then defined both semantically and proof-theoretically which selects the consistent contents answering to a majority principle. The results obtained are proven to be equivalent to a standard majority operator for bases with partial support.

}, doi = {http://dx.doi.org/10.1007/s11229-008-9370-2}, author = {Primiero, Giuseppe and Meheus, Joke} } @article {primieromodel, title = {A model for processing updates with inconsistent information on propositional databases}, year = {2008}, institution = { College Publications}, abstract = {

In the present paper a model for information update on propositional databases is formulated using the standard format of Adaptive Logics. The core structure of the update procedure is represented by the ab- normal expressions of the language that formalize received information contradicting previous contents. The strategy de ned to restrict abnor- malities works by establishing, at each stage of the process, the most re- cent and reliable information, updating constantly the base and removing older data.

}, author = {Primiero, Giuseppe} } @article {Primiero2007, title = {A modal language for contextual computations}, year = {2007}, month = {June}, abstract = {

In this paper, we present a modal language for contextual computing, corresponding to the fragment of constructive ΚΤ with necessity and pos- sibility operators. We interpret absolute and contextual computations as difierent modes of verifying the truth of propositions. The semantics of the language L cc interprets absolute computations by a direct verification function valid in every state; contextual computations are interpreted in terms of a verification function valid under unverified information. Modal- ities are used to express extensions of contexts in order to de ne local and global validity. This semantics has a (weak) monotonicity property, de- pending on satisfaction of processes in contexts. In the corresponding axiomatic system cΚΤ a restricted version of the deduction theorem for globally valid formulas holds, soundness and completeness are proven and decidability is shown to hold for the necessitation fragment of the language by a restricted finite model property..

}, author = {Primiero, Giuseppe} }