@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c year>=2009 /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@inproceedings{AnconaEtAl16,
  author = {Ancona, D. and
               Ferrando, A. and
               Mascardi, V.},
  title = {Comparing Trace Expressions and Linear Temporal Logic for Runtime
               Verification},
  booktitle = {Theory and Practice of Formal Methods - Essays Dedicated to Frank
               de Boer on the Occasion of His 60th Birthday},
  pages = {47--64},
  year = {2016},
  abstract = {{Trace expressions are a compact and expressive formalism, initially devised 
for runtime verification of agent interactions in multiagent systems, which has been
successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms, 
and generalized to support runtime verification of different kinds of properties and systems.

In this paper we formally compare the expressive power of trace expressions with
the Linear Temporal Logic (LTL), a formalism widely adopted in runtime verification.  
We show that any LTL formula can be translated into a trace expression 
which is equivalent from the point of view of runtime verification.
Since trace expressions are able to express and verify sets of traces that
are not context-free, we can derive that in the context of runtime verification 
trace expressions are more expressive than LTL.
}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaEtAlFdB16.pdf},
  keywords = {agents, behavioral-types,runtime-verification}
}
@inproceedings{AnconaBFMT14,
  author = {Ancona, Davide and
               Briola, Daniela  and
               El Fallah{-}Seghrouchni, Amal  and
               Mascardi, Viviana and
               Taillibert, Patrick},
  title = {Exploiting Prolog for Projecting Agent Interaction Protocols},
  booktitle = {Proceedings of the 29th Italian Conference on Computational Logic,
               Torino, Italy, June 16-18, 2014.},
  pages = {30--45},
  year = {2014},
  abstract = {{Constrained global types are a powerful means to represent agent interaction protocols. In our recent research we demonstrated that they can be used to represent complex protocols in a very compact way, and we exploited them to dynamically verify correct implementation of a protocol in a real MAS framework, Jason.
The main drawback of our previous approach is the full centralization of the monitoring activity which is delegated to a unique monitor agent.
This approach works well for MASs with few agents, but could become unsuitable in communication-intensive and highly-distributed MASs where hundreds of agents should be monitored.    
In this paper we define an algorithm for projecting a constrained global type onto a set of agents Ags, 
by restricting it to the interactions involving agents in Ags, so that the outcome of the algorithm is
another constrained global type that can be safely used for verifying the compliance of the sub-system Ags to the protocol specified by the original constrained global type.
The projection mechanism is implemented in SWI Prolog and is the first step towards distributing the monitoring activity, making it safer and more efficient: the compliance of a MAS to a protocol could be dynamically verified by suitably partitioning the agents of the MAS into small sets 
of agents, and by assigning to each partition Ags a local monitor agent which checks all interactions involving Ags against the projected constrained global type. 
We leave for further investigation the problem of finding suitable partitions of agents in a MAS, to guarantee that
verification through projected types and distributed agents is equivalent to verification
performed by a single centralized monitor with a unique global type.}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaBFMT14.pdf},
  keywords = {agents, behavioral-types,runtime-verification}
}
@inproceedings{BonsangueEtAl14,
  author = {Bonsangue, M. and
               Rot, J. and
               Ancona, D. and
               de Boer, F.S. and
               Rutten, J.},
  editor = {Esparza, J. and
               Fraigniaud, P. and
               Husfeldt, T. and
               Koutsoupias, E.},
  title = {A Coalgebraic Foundation for Coinductive Union Types},
  booktitle = {{Automata, Languages, and Programming - 41st International
               Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11,
               2014, Proceedings, Part II}},
  publisher = {Springer},
  series = {{Lecture Notes in Computer Science}},
  volume = {8573},
  year = {2014},
  pages = {62-73},
  keywords = {{coinduction}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/BonsangueEtAl14.pdf},
  abstract = {{This paper introduces a coalgebraic foundation for coinductive types, interpreted as sets of values and extended
with set theoretic union. We give a sound and complete characterization of semantic subtyping in terms of
inclusion of maximal traces. Further, we provide a technique for reducing subtyping to inclusion between sets of
finite traces, based on approximation. We obtain inclusion of tree languages as a sound and complete
method to show semantic subtyping of recursive types with basic types, product and union, interpreted coinductively.
}}
}
@article{MascardiEtAl14,
  keywords = {{agents}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/MABBR@WIAS14.pdf},
  author = {Mascardi, V. and Ancona, D. and Barbieri, M. and Bordini, R. H. and Ricci, A.},
  title = {{CooL-AgentSpeak: Endowing AgentSpeak-DL agents with plan exchange and ontology services}},
  journal = {{Web Intelligence and Agent Systems}},
  volume = {12},
  number = {1},
  pages = {83-107},
  year = {2014},
  abstract = { In this paper we present CooL-AgentSpeak, an extension of
  AgentSpeak-DL with plan exchange and ontology services.  In
  CooL-AgentSpeak, the search for an ontologically relevant plan is no
  longer limited to the agent's local plan library but is carried out
  in the other agents' libraries too, according to a cooperation
  strategy, and it is not based solely on unification and on the
  subsumption relation between concepts, but also on ontology
  matching. Belief querying and updating also take advantage of
  ontological reasoning and matching.}
}
@article{AnconaDovier13,
  keywords = {{coinduction}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaDovier14.pdf},
  author = {Ancona, D. and Dovier, A.},
  title = {{co-LP: Back to the Roots}},
  journal = {{Theory and Practice of Logic Programming }},
  volume = {13},
  number = {4-5-Online-Supplement},
  year = {2013},
  abstract = {Recently, several papers dealing with co-inductive logic
programming have been proposed, dealing with pure Prolog and
constraint logic programming, with and without negation.
In this paper we revisit and use, as much as possible,
some fundamental results developed in the Eighties
to analyze the foundations,
and  to clarify the possibilities but also
the intrinsic theoretical limits of this programming paradigm.
}
}
@inproceedings{AnconaCorradi14,
  booktitle = {{ECOOP 2014 - Object-Oriented Programming}},
  keywords = {{objects,types,coinduction}},
  note = {{To appear}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/CompleteCoinductiveSubtyping.pdf},
  author = {Ancona, D. and Corradi, A.},
  title = {{Sound and complete subtyping between coinductive types for object-oriented languages}},
  year = {2014},
  abstract = {Structural subtyping is an important notion for effective static type analysis;
it can be defined either axiomatically by a collection of subtyping rules, or by means of set inclusion between type interpretations, following
the semantic subtyping approach, which is more intuitive, and allows simpler proofs of the expected properties of the subtyping relation.  

In object-oriented programming, recursive types typically correspond to inductively defined data structures, and subtyping is defined axiomatically; 
however, in object-oriented languages objects can also be cyclic, but inductive types
cannot represent them as precisely as happens for coinductive types. 

We study semantic subtyping between coinductive types with records and unions, which are particularly interesting for object-oriented programming, 
show cases where it allows more precise type analysis, and develop a sound and complete effective algorithm for deciding it.
To our knowledge, this is the first proposal for a sound and complete algorithm for semantic subtyping between coinductive types.
}
}
@inproceedings{AnconaEtAl13a,
  booktitle = {{ACM Symposium on Applied Computing (SAC 2013)}},
  keywords = {{agents, behavioral-types,runtime-verification}},
  note = {{Poster paper}},
  author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
  title = {{Constrained Global Types for Dynamic Checking of Protocol Conformance in Multi-Agent Systems}},
  pages = {1-3},
  year = {2013},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-SAC13.pdf},
  abstract = {Global types are behavioral types for specifying and verifying multiparty 
interactions between distributed components, inspired by the process algebra approach. 

In this paper we extend the formalism of global types in multi-agent systems resulted from our previous work with a mechanism for easily expressing constrained shuffle of message sequences; accordingly, we extend the semantics to include the newly introduced feature, and show the expressive power of these ``constrained global types''.
}
}
@article{AnconaCOMLAN13,
  institution = {{DIBRIS - Universit{\`{a}} di Genova}},
  keywords = {{coinduction,corecursion}},
  note = {{Extended version of \url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#AnconaSAC12}{SAC 2012}}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/COMLAN13.pdf},
  author = {Ancona, D.},
  title = {{Regular corecursion in Prolog}},
  journal = {{Computer Languages, Systems \& Structures}},
  volume = {39},
  number = {4},
  pages = {142-162},
  year = {2013},
  abstract = {Corecursion is the ability of defining a function that
                   produces some infinite data in terms of the function
                   and the data itself, as supported by lazy evaluation.
                   However, in languages such as Haskell strict operations
                   fail to terminate even on infinite regular data, that
                   is, cyclic data. Regular corecursion is naturally
                   supported by coinductive Prolog, an extension where
                   predicates can be interpreted either inductively or
                   coinductively, that has proved to be useful for formal
                   verification, static analysis and symbolic evaluation
                   of programs. In this paper we use the meta-programming
                   facilities offered by Prolog to propose extensions to
                   coinductive Prolog aiming to make regular corecursion
                   more expressive and easier to program with. First, we
                   propose a new interpreter to solve the problem of
                   non-terminating failure as experienced with the
                   standard semantics of coinduction (as supported, for
                   instance, in SWI-Prolog). Another problem with the
                   standard semantics is that predicates expressed in
                   terms of existential quantification over a regular term
                   cannot directly defined by coinduction; to this aim, we
                   introduce finally clauses, to allow more flexibility in
                   coinductive definitions. Then we investigate the
                   possibility of annotating arguments of coinductive
                   predicates, to restrict coinductive definitions to a
                   subset of the arguments; this allows more efficient
                   definitions, and further enhance the expressive power
                   of coinductive Prolog. We investigate the effectiveness
                   of such features by showing different example programs
                   manipulating several kinds of cyclic values, ranging
                   from automata and context free grammars to graphs and
                   repeating decimals; the examples show how computations
                   on cyclic values can be expressed with concise and
                   relatively simple programs. The semantics defined by
                   these vanilla meta-interpreters are an interesting
                   starting point for a more mature design and
                   implementation of coinductive Prolog. }
}
@inproceedings{AZ_FTfJP13,
  booktitle = {{Formal techniques for Java-like programs (FTfJP13)}},
  keywords = {{objects, coinduction, corecursion}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-FTfJP13.pdf},
  author = {Ancona, D. and Zucca, E.},
  title = {{Safe Corecursion in coFJ}},
  pages = {2:1--2:7},
  year = {2013},
  abstract = {In previous work we have presented coFJ, an extension
                   to Featherweight Java that promotes coinductive
                   programming, a sub-paradigm expressly devised to ease
                   high-level programming and reasoning with cyclic data
                   structures. The coFJ language supports cyclic objects
                   and regularly corecursive methods, that is, methods
                   whose invocation terminates not only when the
                   corresponding call trace is finite (as happens with
                   ordinary recursion), but also when such a trace is
                   infinite but cyclic, that is, can be specified by a
                   regular term, or, equivalently, by a finite set of
                   recursive syntactic equations. In coFJ it is not easy
                   to ensure that the invocation of a corecursive method
                   will return a well-defined value, since the recursive
                   equations corresponding to the regular trace of the
                   recursive calls may not admit a (unique) solution; in
                   such cases we say that the value returned by the method
                   call is undetermined. In this paper we propose two new
                   contributions. First, we design a simpler construct for
                   defining corecursive methods and, correspondingly,
                   provide a more intuitive operational semantics. For
                   this coFJ variant, we are able to define a type system
                   that allows the user to specify that certain
                   corecursive methods cannot return an undetermined
                   value; in this way, it is possible to prevent unsafe
                   use of such a value. The operational semantics and the
                   type system of coFJ are fully formalized, and the
                   soundness of the type system is proved. }
}
@inproceedings{Ancona_FTfJP14,
  booktitle = {{Formal techniques for Java-like programs (FTfJP14)}},
  keywords = {{semantics, types, objects, coinduction}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/Ancona-FTfJP14.pdf},
  author = {Ancona, D.},
  title = {{How to Prove Type Soundness of Java-like Languages Without Forgoing Big-step Semantics}},
  pages = {1:1--1:6},
  year = {2014},
  articleno = {1},
  publisher = {ACM},
  abstract = {Small-step operational semantics is the most commonly employed formalism for
proving type soundness of statically typed programming languages, because 
of its ability to distinguish stuck from non-terminating computations,
as opposed to big-step operational semantics.

Despite this, big-step operational semantics is more abstract, and more
useful for specifying interpreters. 

In previous work we have proposed a new proof technique to prove type soundness
of a Java-like language expressed in terms of its big-step operational semantics.
However the presented proof is rather involved, since it
requires showing that the set of proof trees defining the semantic judgment forms a complete metric space
when equipped with a specific distance function.
  
In this paper we propose a more direct and abstract approach that exploits a standard and general compactness property
of the metric space of values, that allows approximation of the coinductive big-step semantics in terms of the small-step one;
in this way type soundness can be proved by standard mathematical induction.
}
}
@inproceedings{AGZ_ITRS12,
  booktitle = {{Intersection Types and Related Systems (ITRS 2013)}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AGZ-ITRS13.pdf},
  author = {Ancona, D. and Giannini, P. and Zucca, E.},
  title = {{Reconciling positional and nominal binding}},
  pages = {81-93},
  year = {2013},
  abstract = {We define an extension of the simply-typed lambda
                   calculus where two different binding mechanisms, by
                   position and by name, nicely coexist. In the former, as
                   in standard lambda calculus, the matching betweeen
                   parameter and argument is done on a positional basis,
                   hence alpha-equivalence holds, whereas in the latter it
                   is done on a nominal basis. The two mechanisms also
                   respectively correspond to static binding, where the
                   existence and type compatibility of the argument are
                   checked at compile-time, and dynamic binding, where
                   they are checked at runtime.}
}
@inproceedings{AMP-SAC12,
  author = {Ancona, D. and Mascardi, V. and Pavarino, O.},
  title = {Ontology-based documentation extraction for
                   semi-automatic migration of {J}ava code},
  booktitle = {A{CM} {S}ymposium on {A}pplied {C}omputing ({SAC}
                   2012)},
  editor = {Ossowski, S. and Lecca, P.},
  pages = {1137--1143},
  publisher = {ACM},
  abstract = {Migrating libraries is not a trivial task, even under
                   the simplest assumption of a downward compatible
                   upgrade. We propose a novel approach to partially
                   relieve programmers from this task, based on the simple
                   observation that class, method and field names and
                   comments contained in a Java library should be a good
                   approximation of its semantics, and that code migration
                   requires knowing the semantic similarities between the
                   two libraries. Following this assumption, we borrow the
                   main concepts and notions from the Semantic Web, and
                   show how (1) an ontology can be automatically generated
                   from the relevant information extracted from the code
                   of the library; (2) semantic similarities between two
                   different libraries can be found by running a
                   particular ontology matching (a.k.a. ontology
                   alignment) algorithm on the two ontologies extracted
                   from the libraries. The main advantages of the approach
                   are that ontology extraction can be fully automated,
                   without adding ad-hoc code annotations, and that
                   results and tools produced by the Semantic Web research
                   community can be directly re-used for our purposes.
                   Experiments carried out even with simple and efficient
                   freely available matchers show that our approach is
                   promising, even though it would benefit from the use of
                   more advanced ontology matchers possibly integrated
                   with a component for checking type compatibility of the
                   computed alignments. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AMP-SAC12.pdf},
  keywords = {agents, ontologies, refactoring},
  year = 2012
}
@inproceedings{AnconaSAC12,
  author = {Ancona, D.},
  title = {Regular corecursion in {P}rolog},
  booktitle = {A{CM} {S}ymposium on {A}pplied {C}omputing ({SAC}
                   2012)},
  editor = {Ossowski, S. and Lecca, P.},
  pages = {1897--1902},
  abstract = {Co-recursion is the ability of defining a function
                   that produces some infinite data in terms of the
                   function and the data itself, and is typically
                   supported by languages with lazy evaluation. However,
                   in languages as Haskell strict operations fail to
                   terminate even on infinite regular data. Regular
                   co-recursion is naturally supported by co-inductive
                   Prolog, an extension where predicates can be
                   interpreted either inductively or co-inductively, that
                   has proved to be useful for formal verification, static
                   analysis and symbolic evaluation of programs. In this
                   paper we propose two main alternative vanilla
                   meta-interpreters to support regular co-recursion in
                   Prolog as an interesting programming style in its own
                   right, able to elegantly solve problems that would
                   require more complex code if conventional recursion
                   were used. In particular, the second meta-interpreters
                   avoids non termination in several cases, by restricting
                   the set of possible answers. The semantics defined by
                   these vanilla meta-interpreters are an interesting
                   starting point to study new semantics able to support
                   regular co-recursion for non logical languages. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaSAC12.pdf},
  keywords = {coinduction,corecursion},
  year = 2012
}
@inproceedings{AnconaECOOP12,
  author = {Ancona, D.},
  title = {Soundness of {O}bject-{O}riented {L}anguages with
                   {C}oinductive {B}ig-{S}tep {S}emantics},
  booktitle = {E{COOP} 2012 - {O}bject-{O}riented {P}rogramming},
  editor = {Noble, J.},
  volume = {7313},
  pages = {459--483},
  publisher = {Springer},
  abstract = {It is well known that big-step operational semantics
                   are not suitable for proving soundness of type systems,
                   because of their inability to distinguish stuck from
                   non-terminating computations. We show how this problem
                   can be solved by interpreting coinductively the rules
                   for the standard big-step operational semantics of a
                   Java-like language, thus making the claim of soundness
                   more intuitive: whenever a program is well-typed, its
                   coinductive operational semantics returns a value.
                   Indeed, coinduction allows non-terminating computations
                   to return values; this is proved by showing that the
                   set of proof trees defining the semantic judgment forms
                   a complete metric space when equipped with a proper
                   distance function. In this way, we are able to prove
                   soundness of a nominal type system w.r.t. the
                   coinductive semantics. Since the coinductive semantics
                   is sound w.r.t. the usual small-step operational
                   semantics, the standard claim of soundness can be
                   easily deduced. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaECOOP12.pdf},
  keywords = {semantics, types, objects, coinduction},
  year = 2012
}
@inproceedings{AL-TCS12,
  author = {Ancona, D. and Lagorio, G.},
  title = {Static single information form for abstract
                   compilation},
  booktitle = {Theoretical {C}omputer {S}cience ({IFIP} {TCS} 2012)},
  editor = {Baeten, J. C.M. and Ball, T. and de Boer, F. S.},
  volume = {7604},
  series = {Lecture Notes in Computer Science},
  pages = {10--27},
  publisher = {Springer},
  abstract = {In previous work we have shown that more precise type
                   analysis can be achieved by exploiting union types and
                   static single assignment (SSA) intermediate
                   representation (IR) of code. In this paper we exploit
                   static single information (SSI), an extension of SSA
                   proposed in literature and adopted by some compilers,
                   to allow assignments of more precise types to variables
                   in conditional branches. In particular, SSI can be
                   exploited rather easily and effectively to infer more
                   precise types in dynamic object-oriented languages,
                   where explicit runtime typechecking is frequently used.
                   We show how the use of SSI form can be smoothly
                   integrated with abstract compilation, our approach to
                   static type analysis. In particular, we define abstract
                   compilation based on union and nominal types for a
                   simple dynamic object-oriented language in SSI form
                   with a runtime typechecking operator, to show how
                   precise type inference can be.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AL-TCS12.pdf},
  keywords = {objects,types,coinduction},
  year = 2012
}
@inproceedings{AZ-CoLP12,
  author = {Ancona, D. and Zucca, E.},
  title = {Translating Corecursive {F}eatherweight {J}ava in
                   Coinductive Logic Programming},
  booktitle = {{Co-LP} 2012 - A workshop on {C}oinductive {L}ogic
                   {P}rogramming},
  abstract = {Corecursive FeatherWeight Java (coFJ) is a recently
                   proposed extension of the calculus FeatherWeight Java
                   (FJ), supporting cyclic objects and regular recursion,
                   and explicitly designed to promote a novel programming
                   paradigm inspired by coinductive Logic Programming
                   (coLP), based on coinductive, rather than inductive,
                   interpretation of recursive function definitions. We
                   present a slightly modified version of coFJ where the
                   application of a coinductive hypothesis can trigger the
                   evaluation of a specific expression at declaration,
                   rather than at use site. Following an approach inspired
                   by abstract compilation, we then show how coFJ can be
                   directly translated into coLP, when coinductive SLD is
                   extended with a similar feature for explicitly solving
                   a goal when a coinductive hypothesis is applied. Such a
                   translation is quite compact and, besides showing the
                   direct relation between coFJ and coinductive Prolog,
                   provides a first prototypical but simple and effective
                   implementation of coFJ.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-CoLP12.pdf},
  keywords = {objects, coinduction, corecursion},
  year = 2012
}
@inproceedings{ABM-ICTCS12,
  author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
  title = {Global {T}ypes for {D}ynamic {C}hecking of {P}rotocol
                   {C}onformance of {M}ulti-{A}gent {S}ystems ({E}xtended
                   {A}bstract)},
  booktitle = {13th {I}talian {C}onference on {T}heoretical
                   {C}omputer {S}cience ({ICTCS} 2012)},
  editor = {Massazza, P.},
  pages = {39--43},
  abstract = {In this paper we investigate the theoretical
                   foundations of global types for dynamic checking of
                   protocol compliance in multi-agents systems and we
                   extend the formalism by introducing a concatenation
                   operator that allows a significant enhancement of the
                   expressive power of global types. As examples, we show
                   how two non trivial protocols can be compactly
                   represented in the formalism: a ping-pong protocol, and
                   an alternating bit protocol, in the version proposed by
                   Deni\backslash{}'elou and Yoshida. Both protocols
                   cannot be specified easily (if at all) by other global
                   type frameworks, while in our approach they can be
                   expressed by two deterministic types (in a sense made
                   precise in the sequel) that can be effectively employed
                   for dynamic checking of the conformance to the
                   protocol.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-ICTCS12.pdf},
  keywords = {agents, behavioral-types,runtime-verification},
  year = 2012
}
@inproceedings{AZ-FTfJP12,
  author = {Ancona, D. and Zucca, E.},
  title = {Corecursive {F}eatherweight {J}ava},
  booktitle = {Formal techniques for {J}ava-like programs
                   ({FT}f{JP}12)},
  abstract = {Despite cyclic data structures occur often in many
                   application domains, object-oriented programming
                   languages provide poor abstraction mechanisms for
                   dealing with cyclic objects. Such a deficiency is
                   reflected also in the research on theoretical
                   foundation of object-oriented languages; for instance,
                   Featherweigh Java (FJ), which is one of the most
                   widespread object-oriented calculi, does not allow
                   creation and manipulation of cyclic objects. We propose
                   an extension to Featherweight Java, called coFJ, where
                   it is possible to define cyclic objects, \{abstractly
                   corresponding to regular terms\}, and where an
                   abstraction mechanism, called regular corecursion, is
                   provided for supporting implementation of coinductive
                   operations on cyclic objects. We formally define the
                   operational semantics of coFJ, and provide a handful of
                   examples showing the expressive power of regular
                   corecursion; such a mechanism promotes a novel
                   programming style particularly well-suited for
                   implementing cyclic data structures, and for supporting
                   coinductive reasoning. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-FTfJP12.pdf},
  keywords = {objects, coinduction, corecursion},
  year = 2012
}
@inproceedings{ADM-DALT12,
  author = {Ancona, D. and Drossopoulou, S. and Mascardi, V.},
  title = {{Automatic Generation of Self-Monitoring MASs from
                   Multiparty Global Session Types in Jason}},
  booktitle = {Declarative agent languages and technologies (DALT
                   2012).},
  pages = {1--20},
  publisher = {Springer},
  abstract = {Global session types are behavioral types designed for
                   specifying in a compact way multiparty interactions
                   between distributed components, and verifying their
                   correctness. We take advantage of the fact that global
                   session types can be naturally represented as cyclic
                   Prolog terms - which are directly supported by the
                   Jason implementation of AgentSpeak - to allow simple
                   automatic generation of self-monitoring MASs: given a
                   global session type specifying an interaction protocol,
                   and the implementation of a MAS where agents are
                   expected to be compliant with it, we define a procedure
                   for automatically deriving a self-monitoring MAS. Such
                   a generated MAS ensures that agents conform to the
                   protocol at run-time, by adding a monitor agent that
                   checks that the ongoing conversation is correct w.r.t.
                   the global session type. The feasibility of the
                   approach has been experimented in Jason for a
                   non-trivial example involving recursive global session
                   types with alternative choice and fork type
                   constructors. Although the main aim of this work is the
                   development of a unit testing framework for MASs, the
                   proposed approach can be also extended to implement a
                   framework supporting self-recovering MASs.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ADM-DALT12.pdf},
  keywords = {agents, behavioral-types, runtime-verification},
  year = 2012
}
@inproceedings{ACLD10-FoVeOOS10,
  author = {Ancona, D. and Corradi, A. and Lagorio, G. and
                   Damiani, F.},
  title = {Abstract compilation of object-oriented languages into
                   coinductive {CLP}({X}): can type inference meet
                   verification?},
  booktitle = {Formal {V}erification of {O}bject-{O}riented
                   {S}oftware {I}nternational {C}onference, {F}o{V}e{OOS}
                   2010, {P}aris, {F}rance, {J}une 28-30, 2010,
                   \textbf{{R}evised {S}elected {P}apers}},
  editor = {Beckert, B. and March\'e, C.},
  volume = {6528},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  abstract = {This paper further investigates the potential and
                   practical applicability of abstract compilation in two
                   different directions. First, we formally define an
                   abstract compilation scheme for precise prediction of
                   uncaught exceptions for a simple Java-like language;
                   besides the usual user declared checked exceptions, the
                   analysis covers the runtime ClassCastException. Second,
                   we present a general implementation schema for abstract
                   compilation based on coinductive CLP with variance
                   annotation of user-defined predicates, and propose an
                   implementation based on a Prolog prototype
                   meta-interpreter, parametric in the solver for the
                   subtyping constraints.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ACLD10-FoVeOOS10.pdf},
  keywords = {objects,types,coinduction},
  year = 2011
}
@article{AL-RAIRO11,
  author = {D. Ancona and G. Lagorio},
  title = {Idealized coinductive type systems for imperative
                   object-oriented programs},
  journal = {RAIRO - Theoretical Informatics and Applications},
  volume = {45},
  number = {1},
  pages = {3-33},
  abstract = {In recent work we have proposed a novel approach to
                   define idealized type systems for object-oriented
                   languages, based on abstract compilation of programs
                   into Horn formulas which are interpreted w.r.t. the
                   coinductive (that is, the greatest) Herbrand model. In
                   this paper we investigate how this approach can be
                   applied also in the presence of imperative features.
                   This is made possible by con- sidering a natural
                   translation of Static Single Assignment intermediate
                   form programs into Horn formulas, where phi functions
                   correspond to union types.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/RAIRO.pdf},
  keywords = {objects,types,coinduction},
  url = {http://www.rairo-ita.org},
  year = 2011
}
@inproceedings{AnconaFTfJP11,
  author = {Ancona, D.},
  title = {Coinductive big-step operational semantics for type
                   soundness of {J}ava-like languages},
  booktitle = {Formal {T}echniques for {J}ava-like {P}rograms
                   ({FT}f{JP}11)},
  pages = {5:1--5:6},
  publisher = {ACM},
  abstract = {We define a coinductive semantics for a simple
                   Java-like language by simply interpreting coinductively
                   the rules of a standard big-step operational semantics.
                   We prove that such a semantics is sound w.r.t. the
                   usual small-step operational semantics, and then prove
                   soundness of a conventional nominal type system w.r.t.
                   the coinductive semantics. From these two results,
                   soundness of the type system w.r.t. the small-step
                   semantics can be easily deduced. This new proposed
                   approach not only opens up new possibilities for
                   proving type soundness, but also provides useful
                   insights on the connection between coinductive big-step
                   operational semantics and type systems.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTfJP11.pdf},
  isbn = {978-1-4503-0893-9},
  keywords = {semantics, types, objects, coinduction},
  year = 2011
}
@inproceedings{MA-DALT11,
  author = {Mascardi, V. and Ancona, D},
  title = {1000 Years of Coo-{BDI}},
  booktitle = {{D}eclarative {A}gent {L}anguages and {T}echnologies
                   {IX} - 9th {I}nternational {W}orkshop, {DALT} 2011,
                   Revised Selected and Invited Papers},
  pages = {95-101},
  abstract = {The idea of extending the BDI architecture with
                   cooperativity started shaping in 2003 when two
                   independent proposals to support cooperation in a BDI
                   setting were presented at DALT. One proposal, Coo-BDI,
                   extended the BDI architecture by allowing agents to
                   cooperate by exchanging and sharing plans in a quite
                   flexible way; the other extended the BDI operational
                   semantics for introducing speech-act based
                   communication, including primitives for plan exchange.
                   Besides allowing a natural and seamless integration
                   with speech-act based communication for BDI languages,
                   the intuitions behind Coo-BDI have proved to be
                   promising and attractive enough to give rise to new
                   investigations. In this retrospective review we discuss
                   papers that were influenced by Coo-BDI and we outline
                   other potential developments for future research.},
  keywords = {agents, behavioral-types},
  ftp = {http://www.disi.unige.it/person/MascardiV/Download/1000YearsCooBDI.pdf},
  year = 2011
}
@inproceedings{MABR-IAT11,
  author = {Mascardi, V. and Ancona, D. and Bordini, R. H. and
                   Ricci, A.},
  title = {CooL-{A}gent{S}peak: {E}nhancing {A}gent{S}peak-{DL}
                   {A}gents with {P}lan {E}xchange and {O}ntology
                   {S}ervices},
  booktitle = {Proceedings of the 2011 {IEEE}/{WIC}/{ACM}
                   {I}nternational {C}onference on {I}ntelligent {A}gent
                   {T}echnology, {IAT} 2011},
  pages = {109-116},
  abstract = {In this paper we present CooL-AgentSpeak, an extension
                   of AgentSpeak-DL with plan exchange and ontology
                   services. In CooL-AgentSpeak, the search for a plan is
                   no longer limited to the agent's local plan library but
                   is carried out in the other agents' libraries too,
                   according to a cooperation strategy, and it is not
                   based solely on unification and on the subsumption
                   relation between concepts, but also on ontology
                   matching. Belief querying and updating take advantage
                   of ontological reasoning and matching as well.},
  keywords = {agents, behavioral-types},
  ftp = {http://www.disi.unige.it/person/MascardiV/Download/IAT2011.pdf},
  year = 2011
}
@techreport{AL-10-11,
  author = {Ancona, D. and Lagorio, G.},
  title = {On sound and complete axiomatization of coinductive
                   subtyping for object-oriented languages},
  institution = {DISI},
  note = {Submitted for journal publication. Extended version of
                   \url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#AL-FTfJP10}{FTfJP10}},
  abstract = {Coinductive abstract compilation is a novel technique,
                   which has been recently introduced for defining precise
                   type systems for object- oriented languages. In this
                   approach, type inference consists in translating the
                   program to be analyzed into a Horn formula f, and in
                   resolving a certain goal w.r.t. the coinductive (that
                   is, the greatest) Herbrand model of f. Type systems
                   defined in this way are idealized, since types and,
                   con- sequently, goal derivations, are not finitely
                   representable. Hence, sound implementable
                   approximations have to rely on the notions of regular
                   types and derivations, and of subtyping and subsumption
                   between types and atoms, respectively. In this paper we
                   address the problem of defining a sound and complete
                   axiomatization of a subtyping relation between
                   coinductive object and union types, defined as set
                   inclusion between type interpretations. Besides being
                   an important theoretical result, completeness is useful
                   for reasoning about possible implementations of the
                   subtyping relation, when restricted to regular types.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AL10-11.pdf},
  keywords = {objects,types,coinduction},
  month = nov,
  year = 2010
}
@techreport{ACLD10-08-ext,
  author = {Ancona, D. and Corradi, A. and Lagorio, G. and
                   Damiani, F.},
  title = {Abstract compilation of object-oriented languages into
                   coinductive {CLP}({X}): can type inference meet
                   verification? (extended version)},
  institution = {DISI},
  note = {Extended version of \url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#ACLD10-FoVeOOS10}{FoVeOOS10}},
  abstract = {This paper further investigates the potential and
                   practical applicability of abstract compilation in two
                   different directions. First, we formally define an
                   abstract compilation scheme for precise prediction of
                   uncaught exceptions for a simple Java-like language;
                   besides the usual user declared checked exceptions, the
                   analysis covers the runtime ClassCastException. Second,
                   we present a general implementation schema for abstract
                   compilation based on coinductive CLP with variance
                   annotation of user-defined predicates, and propose an
                   implementation based on a Prolog prototype
                   meta-interpreter, parametric in the solver for the
                   subtyping constraints. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ACLD10ext.pdf},
  keywords = {objects,types,coinduction},
  month = aug,
  year = 2010
}
@inproceedings{AL-FTfJP10,
  author = {D. Ancona and G. Lagorio},
  title = {Complete coinductive subtyping for abstract
                   compilation of object-oriented languages},
  booktitle = {F{TFJP} '10: {P}roceedings of the 12th {W}orkshop on
                   {F}ormal {T}echniques for {J}ava-{L}ike {P}rograms},
  series = {ACM Digital Library},
  pages = {1:1--1:7},
  publisher = {ACM},
  abstract = {Coinductive abstract compilation is a novel technique,
                   which has been recently introduced, for defining
                   precise type systems for object-oriented languages. In
                   this approach, type inference consists in translating
                   the program to be analyzed into a Horn formula f, and
                   in resolving a certain goal w.r.t. the coinductive
                   (that is, the greatest) Herbrand model of f. Type
                   systems defined in this way are idealized, since types
                   and, consequently, goal derivations, are not finitely
                   representable. Hence, sound implementable
                   approximations have to rely on the notions of regular
                   types and derivations, and of subtyping and subsumption
                   between types and atoms, respectively. In this paper we
                   address the problem of defining a complete subtyping
                   relation <= between types built on object and union
                   type constructors: we interpret types as sets of
                   values, and investigate on a definition of subtyping
                   such that t\_1 <= t\_2 is derivable whenever the
                   interpretation of t\_1 is contained in the
                   interpretation of t\_2. Besides being an important
                   theoretical result, completeness is useful for
                   reasoning about possible implementations of the
                   subtyping relation, when restricted to regular types. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTfJP10.pdf},
  keywords = {objects,types,coinduction},
  url = {http://portal.acm.org/citation.cfm?id=1924520},
  year = 2010
}
@inproceedings{AL10-GandALF10,
  author = {D. Ancona and G. Lagorio},
  title = {Coinductive subtyping for abstract compilation of
                   object-oriented languages into {H}orn formulas},
  booktitle = {Proceedings of {G}and{ALF} 2010},
  editor = {{Montanari A.} and {Napoli M.} and {Parente M.}},
  volume = {25},
  series = {Electronic Proceedings in Theoretical Computer Science},
  pages = {214--223},
  abstract = {In recent work we have shown how it is possible to
                   define very precise type systems for object-oriented
                   languages by abstractly compiling a program into a Horn
                   formula f. Then type inference amounts to resolving a
                   certain goal w.r.t. the coinductive (that is, the
                   greatest) Herbrand model of f. Type systems defined in
                   this way are idealized, since in the most interesting
                   instantiations both the terms of the coinductive
                   Herbrand universe and goal derivations cannot be
                   finitely represented. However, sound and quite
                   expressive approximations can be implemented by
                   considering only regular terms and derivations. In
                   doing so, it is essential to introduce a proper
                   subtyping relation formalizing the notion of
                   approximation between types. In this paper we study a
                   subtyping relation on coinductive terms built on union
                   and object type constructors. We define an
                   interpretation of types as set of values induced by a
                   quite intuitive relation of membership of values to
                   types, and prove that the definition of subtyping is
                   sound w.r.t. subset inclusion between type
                   interpretations. The proof of soundness has allowed us
                   to simplify the notion of contractive derivation and to
                   discover that the previously given definition of
                   subtyping did not cover all possible representations of
                   the empty type. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/GandALF10.pdf},
  keywords = {objects,types,coinduction},
  year = 2010
}
@techreport{AnconaEtAl10,
  author = {Ancona, D. and Corradi, A. and Lagorio, G. and
                   Damiani, F.},
  title = {Abstract compilation of object-oriented languages into
                   coinductive {CLP}({X}): when type inference meets
                   verification},
  institution = {Karlsruhe Institute of Technology},
  note = {Formal {V}erification of {O}bject-{O}riented
                   {S}oftware. {P}apers presented at the {I}nternational
                   {C}onference, {J}une 28-30, 2010, {P}aris, {F}rance},
  abstract = {We propose a novel general approach for defining
                   expressive type systems for object-oriented languages,
                   based on abstract compilation of programs into
                   coinductive constraint logic programs defined on a
                   specific constraint domain X called type domain. In
                   this way, type checking and type inference amount to
                   resolving a certain goal w.r.t. the coinductive (that
                   is, the greatest) Herbrand model of a logic program
                   (that is, a Horn formula) with constraints over a fixed
                   type domain X. In particular, we show an interesting
                   instantiation where the constraint predicates of X are
                   syntactic equality and subtyping over coinductive
                   object and union types. The corresponding type system
                   is so expressive to allow verification of simple
                   properties like data structure invariants. Finally, we
                   show a prototype implementation, written in Prolog, of
                   the inference engine for coinductive CLP(X), which is
                   parametric in the solver for the type domain X.},
  booktitle = {Formal {V}erification of {O}bject-{O}riented
                   {S}oftware. {P}apers presented at the {I}nternational
                   {C}onference, {J}une 28-30, 2010, {P}aris, {F}rance},
  editor = {Beckert, B. and March\'e, C.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FOVEOOS10-preproc.pdf},
  keywords = {objects,types,coinduction},
  publisher = {Karlsruhe},
  series = {Karlsruhe Reports in Informatics (fr\"uher: Interner
                   Bericht. Fakult\"at f\"ur Informatik, Karlsruher
                   Institut f\"ur Technologie) ; 2010,13},
  year = 2010
}
@inproceedings{AnconaMascardi-MALLOW-AWESOME09,
  author = {Ancona, D. and Mascardi, V.},
  title = {Exploiting {A}gents and {O}ntologies for {T}ype- and
                   {M}eaning-{S}afe {A}daptation of {J}ava {P}rograms},
  booktitle = {Proceedings of the {MALLOW}-{AWESOME} 2009 workshop},
  volume = {494},
  publisher = {CEUR Workshop Proceedings},
  abstract = {This paper discusses an application of intelligent
                   software agents and ontologies to solve the problem of
                   semi-automatic porting of Java programs. We have
                   designed a system for aiding users to adapt Java code
                   in a type- and meaning-safe way, when an application
                   has to migrate to new libraries which are not fully
                   compatible with the legacy ones. To achieve this, we
                   propose an approach based on an integration of the two
                   type-theoretic notions of subtyping and type
                   isomorphism with ontology matching. While the former
                   notions are needed to ensure flexible adaptation in the
                   presence of type-safety, the latter supports the user
                   to preserve the meaning of names that appear in the
                   program to be adapted. Intelligent agents control the
                   different components of the system and interact with
                   other agents in order to provide the final user with
                   the semi-automatic porting service he/she required.},
  ftp = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-494/mallowawesomepaper6.pdf},
  keywords = {agents,refactoring},
  year = 2009
}
@inproceedings{CAR-ICOOLPS09,
  author = {Cuni, A. and Ancona, D. and Rigo, A.},
  title = {Faster than {C}\#: efficient implementation of dynamic
                   languages on {.NET}},
  booktitle = {{ICOOOLPS} '09: Proceedings of the 4th workshop on the
                   {I}mplementation, {C}ompilation, {O}ptimization of
                   {O}bject-{O}riented {L}anguages and {P}rogramming
                   {S}ystems},
  pages = {26--33},
  address = {New York, NY, USA},
  publisher = {ACM},
  abstract = {The Common Language Infrastructure (CLI) is a virtual
                   machine expressly designed for implementing statically
                   typed languages such as C\#, therefore programs written
                   in dynamically typed languages are typically much
                   slower than C\# when executed on .NET. Recent
                   developments show that Just In Time (JIT) compilers can
                   exploit runtime type information to generate quite
                   efficient code. Unfortunately, writing a JIT compiler
                   is far from being simple. In this paper we report our
                   positive experience with automatic generation of JIT
                   compilers as supported by the PyPy infrastructure, by
                   focusing on JIT compilation for .NET. Following this
                   approach, we have in fact added a second layer of JIT
                   compilation, by allowing dynamic generation of more
                   efficient .NET bytecode, which in turn can be compiled
                   to machine code by the .NET JIT compiler. The main and
                   novel contribution of this paper is to show that this
                   two-layers JIT technique is effective, since programs
                   written in dynamic languages can run on .NET as fast as
                   (and in some cases even faster than) the equivalent C\#
                   programs. The practicality of the approach is
                   demonstrated by showing some promising experiments done
                   with benchmarks written in a simple dynamic language. },
  doi = {http://doi.acm.org/10.1145/1565824.1565828},
  ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ICOOOLPS09.pdf},
  isbn = {978-1-60558-541-3},
  keywords = {objects,dynamicLang},
  location = {Genova, Italy},
  year = 2009
}
@inproceedings{ALZ-TYPES08,
  author = {Ancona, D. and Lagorio, G. and Zucca, E.},
  title = {Type inference by coinductive logic programming},
  booktitle = {Post-{P}roceedings of {TYPES} 2008},
  editor = {Berardi S., Damiani F., de' Liguoro U.},
  volume = {5497},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  abstract = {We propose a novel approach to constraint-based type
                   inference based on coinductive logic programming. That
                   is, constraint generation corresponds to translation
                   into a conjunction of Horn clauses P, and constraint
                   satisfaction is defined in terms of the maximal
                   coinductive Herbrand model of P. We illustrate the
                   approach by formally defining this translation for a
                   small object-oriented language similar to Featherweight
                   Java, where type annotations in field and method
                   declarations can be omitted. In this way, we obtain a
                   very precise type inference and provide new insights
                   into the challenging problem of type inference for
                   object-oriented programs. Since the approach is
                   deliberately declarative, we define in fact a formal
                   specification for a general class of algorithms, which
                   can be a useful road maps to researchers. Moreover,
                   despite we consider here a particular language, the
                   methodology could be used in general for providing
                   abstract specifications of type inference for different
                   kinds of programming languages.},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ALZ0908.pdf},
  keywords = {objects,types,coinduction},
  year = 2009
}
@inproceedings{AL-ECOOP09,
  author = {Ancona, D. and Lagorio, G.},
  title = {Coinductive type systems for object-oriented languages},
  booktitle = {ECOOP 2009 - Object-Oriented Programming},
  editor = {{S. Drossopoulou}},
  volume = {5653},
  series = {Lecture Notes in Computer Science},
  pages = {2--26},
  publisher = {Springer Verlag},
  note = {\textbf{Best paper prize}},
  abstract = {We propose a novel approach based on coinductive logic
                   to specify type systems of programming languages. The
                   approach consists in encoding programs in Horn formulas
                   which are interpreted w.r.t. their coinductive Herbrand
                   model. We illustrate the approach by first specifying a
                   standard type system for a small object-oriented
                   language similar to Featherweight Java. Then we define
                   an idealized type system for a variant of the language
                   where type annotations can be omitted. The type system
                   involves infinite terms and proof trees not
                   representable in a finite way, thus providing a
                   theoretical limit to type inference of object-oriented
                   programs, since only sound approximations of the system
                   can be implemented. Approximation is naturally captured
                   by the notions of subtyping and subsumption; indeed,
                   rather than increasing the expressive power of the
                   system, as it usually happens, here subtyping is needed
                   for approximating infinite non regular types and proof
                   trees with regular ones. },
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ECOOP09.pdf},
  keywords = {objects,types,coinduction},
  year = 2009
}
@inproceedings{BriolaMascardiAnconaIDC14,
  author = {Briola, D. and
               Mascardi, V. and
               Ancona, D.},
  title = {Distributed Runtime Verification of {JADE} Multiagent Systems},
  booktitle = {Intelligent Distributed Computing {VIII} - Proceedings of the 8th
               International Symposium on Intelligent Distributed Computing, {IDC}
               2014, Madrid, Spain, September 3-5, 2014},
  pages = {81--91},
  year = {2014},
  abstract = {{Verifying that agent interactions in a multiagent system (MAS) are compliant to a given global protocol is of paramount importance for most systems, and is mandatory for safety-critical applications. Runtime verification requires a proper formalism to express such a protocol, a possibly non intrusive mechanism for capturing agent interactions, and a method for verifying that captured interactions are compliant to the global protocol. Projecting the global protocol onto agents' subsets can improve efficiency and fault tolerance by allowing the distribution of the verification mechanism. Since many real MASs are based on JADE, a well known open source platform for MAS development, we implemented a monitor agent that achieves all the goals above using the "Attribute Global Types" (AGT) formalism for representing protocols. Using our JADE monitor we were able to verify FYPA, an extremely complex industrial MAS currently used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations, besides the Alternating Bit and the Iterated Contract Net protocols which are well known in the distributed systems and MAS communities. Depending on the monitored MAS, the performances of our monitor are either comparable or slightly worse than those of the JADE Sniffer because of the logging of the verification activities. Reducing the log files dimension, re-implementing the monitor in a way independent from the JADE Sniffer, and heavily exploiting projections are the three directions we are pursuing for improving the monitor's performances, still keeping all its features. }},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/IDC2014.pdf},
  keywords = {runtime-verification, agents,behavioral-types}
}
@inproceedings{MascardiBriolaAnconaAIIA13,
  author = {Mascardi, V. and
               Briola, D. and
               Ancona, D.},
  title = {On the Expressiveness of Attribute Global Types: The Formalization
               of a Real Multiagent System Protocol},
  booktitle = {AI*IA 2013: Advances in Artificial Intelligence - XIIIth International
               Conference of the Italian Association for Artificial Intelligence,
               Turin, Italy, December 4-6, 2013. Proceedings},
  pages = {300--311},
  year = {2013},
  abstract = {{Attribute global types are a formalism for specifying and dynamically verifying multi-party agents interaction protocols. They allow the multiagent system designer to easily express synchronization constraints among protocol branches and global constraints on sub-sequences of the allowed protocol traces. FYPA (Find Your Path, Agent!) is a multiagent system implemented in Jade currently being used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations. Since information on the station topology and on the current resource allocation is fully distributed, FYPA involves complex negotiation among agents to find a solution in quasi-real time. In this paper we describe the FYPA protocol using both AUML and attribute global types, showing that the second formalism is more concise than the first, besides being unambiguous and amenable for formal reasoning. Thanks to the Prolog implementation of the transition function defining the attribute global type semantic, we are able to generate a large number of protocol traces, and to manually inspect a subset of them to empirically validate that the protocol's formalization is correct. The integration of the Prolog verification mechanism into a Jade monitoring agent extending the Sniffer Agent is under way and will be used to verify the compliance of the actual conversation with the protocol. Keywords: multiagent systems, attribute global types, negotiation, dynamic verification of protocol compliance. }},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AIIA2013.pdf},
  keywords = {runtime-verification, agents,behavioral-types}
}
@article{AnconaDovierFI15,
  author = {Ancona, D. and
               Dovier, A.},
  title = {A Theoretical Perspective of Coinductive Logic Programming},
  journal = {Fundamenta Informaticae},
  volume = {140},
  number = {3-4},
  pages = {221--246},
  year = {2015},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaDovierFI15.pdf},
  doi = {10.3233/FI-2015-1252},
  keywords = {coinduction,logic programming},
  abstract = {{
In this paper we study the semantics of Coinductive Logic Programming and
clarify  its intrinsic computational limits, which prevent, in particular, the definition
of a complete, computable, operational semantics.
We propose a new operational semantics that  allows a simple correctness result
and the definition of a simple meta-interpreter.
We compare, and prove the equivalence, with the operational semantics
defined and used in other papers on this topic.
}}
}
@article{AnconaGianniniZucca16,
  author = {Ancona, D. and
               Giannini, P. and
               Zucca, E.},
  title = {Incremental Rebinding with Name Polymorphism},
  journal = {Electr. Notes Theor. Comput. Sci.},
  volume = {322},
  pages = {19--34},
  year = {2016},
  url = {http://dx.doi.org/10.1016/j.entcs.2016.03.003},
  doi = {10.1016/j.entcs.2016.03.003},
  keywords = {types, components},
  abstract = {{
We propose an extension with name variables of a calculus for incremental rebinding of code introduced in
previous work. Names, which can be either constants or variables, are used as interface of fragments of code
with free variables. Open code can be dynamically rebound by applying a rebinding, which is an association
from names to terms. Rebinding is incremental, since rebindings can contain free variables as well, and
can be manipulated by operators such as overriding and renaming. By using name variables, it is possible
to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly
enhancing expressivity. The type system is correspondingly extended by constrained name-polymorphic
types, where simple inequality constraints prevent conflicts among parametric name interfaces.
}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaGianniniZucca16.pdf}
}
@article{Betty16,
  author = {Ancona, D. and
               Bono, V. and
               Bravetti, M. and
               Campos, J. and
               Castagna, G. and
               Deni{\'{e}}lou, P.~M. and
               Gay, S.~J. and
               Gesbert, N. and
               Giachino, E. and
               Hu, R. and
               Johnsen, E.~B. and
               Martins, F. and
               Mascardi, V. and
               Montesi, F. and
               Neykova, R. and
               Ng, N. and
               Padovani, L. and
               Vasconcelos, V.T. and
               Yoshida, N.},
  title = {Behavioral Types in Programming Languages},
  journal = {Foundations and Trends in Programming Languages},
  volume = {3},
  number = {2-3},
  pages = {95--230},
  year = {2016},
  url = {http://dx.doi.org/10.1561/2500000031},
  doi = {10.1561/2500000031},
  keywords = {runtime-verification, agents,behavioral-types},
  abstract = {{
A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of largescale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.
}},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/behavioralTypes.pdf}
}
@inproceedings{AnconaCorradiFTfJP16,
  author = {Ancona, D. and Corradi, A.},
  title = {A Formal Account of SSA in Java-like Languages},
  booktitle = {Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs},
  series = {FTfJP'16},
  year = {2016},
  pages = {2:1--2:8},
  articleno = {2},
  numpages = {8},
  publisher = {ACM}
}
@inproceedings{AnconaCorradi16,
  author = {Ancona, D. and
               Corradi, A.},
  title = {Semantic subtyping for imperative object-oriented languages},
  booktitle = {{OOPSLA} 2016},
  pages = {568--587},
  year = {2016}
}
@inproceedings{AnconaDagninoZucca17,
  author = {Ancona, D. and Dagnino, F. and Zucca, E.},
  title = {Generalizing inference systems by coaxioms},
  booktitle = {European Symposium on Programming, ESOP 2017},
  year = {2017},
  note = {To appear},
  ftp = {ftp://ftp.disi.unige.it/person/AnconaD/esop17.pdf},
  abstract = {{We introduce a generalized notion of inference system to support 
structural recursion on non well-founded datatypes.
Besides  axioms and inference rules with the usual meaning, a generalized inference system
allows coaxioms, which are, intuitively, axioms which can only be applied "at infinite depth" in a proof tree. 
This notion nicely subsumes standard inference systems and their inductive and coinductive interpretation, while providing more flexibility.
Indeed, the classical results on the existence and constructive characterization of least and greatest fixed points can be extended to our generalized framework, interpreting recursive definitions as fixed points which are not necessarily the least, nor the greatest one. This allows formal reasoning in cases where the inductive and coinductive interpretation do not provide the intended meaning, or  are mixed together. 
}},
  keywords = {{coinduction}}
}
@inproceedings{AnconaFerrandoMascardi17,
  author = {Ancona, D. and
               Ferrando, A. and
               Mascardi, V.},
  title = {Parametric Runtime Verification of Multiagent Systems},
  booktitle = {Proceedings of the 16th Conference on Autonomous Agents and MultiAgent
               Systems, {AAMAS} 2017, S{\~{a}}o Paulo, Brazil, May 8-12, 2017},
  pages = {1457--1459},
  year = {2017},
  keywords = {runtime-verification, agents,behavioral-types},
  abstract = {{
Parametricity is an important feature of a monitoring
system for making runtime verification (RV) more effective,
since, typically, correctness of traces depends on the specific
data values that are carried by the monitored events of the
trace, and that, in general, cannot be predicted statically.
Typically, the correctness of an interaction protocol may
depend on the values exchanged by agents; protocols may
also be parametric in the involved agents, and resources, and
this parametricity is naturally reflected on the data carried
by values.
In this work we propose parametric trace expressions, an
extension to trace expressions, expressly designed for
parametric RV of multiagent systems. Such an extension is
achieved by introducing variables in trace expressions that
are substituted with data values at runtime, when events are
matched during monitoring.
}},
  http = {http://www.disi.unige.it/person/AnconaD/papers/AnconaFerrandoMascardiAAMAS17Parametric.pdf}
}

This file was generated by bibtex2html 1.98.