[1] 
Davide Ancona and Agostino Dovier.
A theoretical perspective of coinductive logic programming.
Fundamenta Informaticae, 140(34):221246, 2015.
[ bib 
DOI 
.pdf ]
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 metainterpreter. We compare, and prove the equivalence, with the operational semantics defined and used in other papers on this topic.

[2] 
Davide Ancona, Daniela Briola, Amal El FallahSeghrouchni, Viviana Mascardi,
and Patrick Taillibert.
Exploiting prolog for projecting agent interaction protocols.
In Proceedings of the 29th Italian Conference on Computational
Logic, Torino, Italy, June 1618, 2014., pages 3045, 2014.
[ bib 
.pdf ]
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 communicationintensive and highlydistributed 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 subsystem 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.

[3] 
M. Bonsangue, J. Rot, D. Ancona, F.S. de Boer, and J. Rutten.
A coalgebraic foundation for coinductive union types.
In J. Esparza, P. Fraigniaud, T. Husfeldt, and E. Koutsoupias,
editors, Automata, Languages, and Programming  41st International
Colloquium, ICALP 2014, Copenhagen, Denmark, July 811, 2014, Proceedings,
Part II, volume 8573 of Lecture Notes in Computer Science, pages
6273. Springer, 2014.
[ bib 
.pdf ]
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.

[4] 
V. Mascardi, D. Ancona, M. Barbieri, R. H. Bordini, and A. Ricci.
CooLAgentSpeak: Endowing AgentSpeakDL agents with plan exchange
and ontology services.
Web Intelligence and Agent Systems, 12(1):83107, 2014.
[ bib 
.pdf ]
In this paper we present CooLAgentSpeak, an extension of AgentSpeakDL with plan exchange and ontology services. In CooLAgentSpeak, 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.

[5] 
D. Ancona and A. Corradi.
Sound and complete subtyping between coinductive types for
objectoriented languages.
In ECOOP 2014  ObjectOriented Programming, 2014.
To appear.
[ bib 
.pdf ]
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.

[6] 
D. Ancona.
How to Prove Type Soundness of Javalike Languages Without Forgoing
Bigstep Semantics.
In Formal techniques for Javalike programs (FTfJP14), pages
1:11:6. ACM, 2014.
[ bib 
.pdf ]
Smallstep 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 nonterminating computations, as opposed to bigstep operational semantics.

[7] 
D. Briola, V. Mascardi, and D. Ancona.
Distributed runtime verification of JADE multiagent systems.
In Intelligent Distributed Computing VIII  Proceedings of the
8th International Symposium on Intelligent Distributed Computing, IDC 2014,
Madrid, Spain, September 35, 2014, pages 8191, 2014.
[ bib 
.pdf ]
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 safetycritical 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, reimplementing 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.

[8] 
D. Ancona and A. Dovier.
coLP: Back to the Roots.
Theory and Practice of Logic Programming ,
13(45OnlineSupplement), 2013.
[ bib 
.pdf ]
Recently, several papers dealing with coinductive 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.

[9] 
D. Ancona, M. Barbieri, and V. Mascardi.
Constrained Global Types for Dynamic Checking of Protocol
Conformance in MultiAgent Systems.
In ACM Symposium on Applied Computing (SAC 2013), pages 13,
2013.
Poster paper.
[ bib 
.pdf ]
Global types are behavioral types for specifying and verifying multiparty interactions between distributed components, inspired by the process algebra approach.

[10] 
D. Ancona.
Regular corecursion in Prolog.
Computer Languages, Systems & Structures, 39(4):142162,
2013.
Extended version of
SAC
2012.
[ bib 
.pdf ]
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 metaprogramming 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 nonterminating failure as experienced with the standard semantics of coinduction (as supported, for instance, in SWIProlog). 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 metainterpreters are an interesting starting point for a more mature design and implementation of coinductive Prolog.

[11] 
D. Ancona and E. Zucca.
Safe Corecursion in coFJ.
In Formal techniques for Javalike programs (FTfJP13), pages
2:12:7, 2013.
[ bib 
.pdf ]
In previous work we have presented coFJ, an extension to Featherweight Java that promotes coinductive programming, a subparadigm expressly devised to ease highlevel 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 welldefined 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.

[12] 
D. Ancona, P. Giannini, and E. Zucca.
Reconciling positional and nominal binding.
In Intersection Types and Related Systems (ITRS 2013), pages
8193, 2013.
[ bib 
.pdf ]
We define an extension of the simplytyped 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 alphaequivalence 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 compiletime, and dynamic binding, where they are checked at runtime.

[13] 
V. Mascardi, D. Briola, and D. Ancona.
On the expressiveness of attribute global types: The formalization of
a real multiagent system protocol.
In AI*IA 2013: Advances in Artificial Intelligence  XIIIth
International Conference of the Italian Association for Artificial
Intelligence, Turin, Italy, December 46, 2013. Proceedings, pages 300311,
2013.
[ bib 
.pdf ]
Attribute global types are a formalism for specifying and dynamically verifying multiparty agents interaction protocols. They allow the multiagent system designer to easily express synchronization constraints among protocol branches and global constraints on subsequences 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 quasireal 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.

[14] 
D. Ancona, V. Mascardi, and O. Pavarino.
Ontologybased documentation extraction for semiautomatic migration
of Java code.
In S. Ossowski and P. Lecca, editors, ACM Symposium on
Applied Computing (SAC 2012), pages 11371143. ACM, 2012.
[ bib 
.pdf ]
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 adhoc code annotations, and that results and tools produced by the Semantic Web research community can be directly reused 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.

[15] 
D. Ancona.
Regular corecursion in Prolog.
In S. Ossowski and P. Lecca, editors, ACM Symposium on
Applied Computing (SAC 2012), pages 18971902, 2012.
[ bib 
.pdf ]
Corecursion 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 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 propose two main alternative vanilla metainterpreters to support regular corecursion 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 metainterpreters avoids non termination in several cases, by restricting the set of possible answers. The semantics defined by these vanilla metainterpreters are an interesting starting point to study new semantics able to support regular corecursion for non logical languages.

[16] 
D. Ancona.
Soundness of ObjectOriented Languages with Coinductive
BigStep Semantics.
In J. Noble, editor, ECOOP 2012  ObjectOriented
Programming, volume 7313, pages 459483. Springer, 2012.
[ bib 
.pdf ]
It is well known that bigstep operational semantics are not suitable for proving soundness of type systems, because of their inability to distinguish stuck from nonterminating computations. We show how this problem can be solved by interpreting coinductively the rules for the standard bigstep operational semantics of a Javalike language, thus making the claim of soundness more intuitive: whenever a program is welltyped, its coinductive operational semantics returns a value. Indeed, coinduction allows nonterminating 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 smallstep operational semantics, the standard claim of soundness can be easily deduced.

[17] 
D. Ancona and G. Lagorio.
Static single information form for abstract compilation.
In J. C.M. Baeten, T. Ball, and F. S. de Boer, editors,
Theoretical Computer Science (IFIP TCS 2012), volume 7604 of
Lecture Notes in Computer Science, pages 1027. Springer, 2012.
[ bib 
.pdf ]
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 objectoriented 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 objectoriented language in SSI form with a runtime typechecking operator, to show how precise type inference can be.

[18] 
D. Ancona and E. Zucca.
Translating corecursive Featherweight Java in coinductive logic
programming.
In CoLP 2012  A workshop on Coinductive Logic
Programming, 2012.
[ bib 
.pdf ]
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.

[19] 
D. Ancona, M. Barbieri, and V. Mascardi.
Global Types for Dynamic Checking of Protocol Conformance
of MultiAgent Systems (Extended Abstract).
In P. Massazza, editor, 13th Italian Conference on
Theoretical Computer Science (ICTCS 2012), pages 3943, 2012.
[ bib 
.pdf ]
In this paper we investigate the theoretical foundations of global types for dynamic checking of protocol compliance in multiagents 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 pingpong protocol, and an alternating bit protocol, in the version proposed by Deni'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.

[20] 
D. Ancona and E. Zucca.
Corecursive Featherweight Java.
In Formal techniques for Javalike programs (FTfJP12),
2012.
[ bib 
.pdf ]
Despite cyclic data structures occur often in many application domains, objectoriented programming languages provide poor abstraction mechanisms for dealing with cyclic objects. Such a deficiency is reflected also in the research on theoretical foundation of objectoriented languages; for instance, Featherweigh Java (FJ), which is one of the most widespread objectoriented 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 wellsuited for implementing cyclic data structures, and for supporting coinductive reasoning.

[21] 
D. Ancona, S. Drossopoulou, and V. Mascardi.
Automatic Generation of SelfMonitoring MASs from Multiparty Global
Session Types in Jason.
In Declarative agent languages and technologies (DALT 2012).,
pages 120. Springer, 2012.
[ bib 
.pdf ]
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 selfmonitoring 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 selfmonitoring MAS. Such a generated MAS ensures that agents conform to the protocol at runtime, 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 nontrivial 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 selfrecovering MASs.

[22] 
D. Ancona, A. Corradi, G. Lagorio, and F. Damiani.
Abstract compilation of objectoriented languages into coinductive
CLP(X): can type inference meet verification?
In B. Beckert and C. Marché, editors, Formal Verification of
ObjectOriented Software International Conference, FoVeOOS
2010, Paris, France, June 2830, 2010, Revised Selected
Papers, volume 6528 of Lecture Notes in Computer Science. Springer
Verlag, 2011.
[ bib 
.pdf ]
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 Javalike 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 userdefined predicates, and propose an implementation based on a Prolog prototype metainterpreter, parametric in the solver for the subtyping constraints.

[23] 
D. Ancona and G. Lagorio.
Idealized coinductive type systems for imperative objectoriented
programs.
RAIRO  Theoretical Informatics and Applications, 45(1):333,
2011.
[ bib 
.pdf 
http ]
In recent work we have proposed a novel approach to define idealized type systems for objectoriented 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.

[24] 
D. Ancona.
Coinductive bigstep operational semantics for type soundness of
Javalike languages.
In Formal Techniques for Javalike Programs
(FTfJP11), pages 5:15:6. ACM, 2011.
[ bib 
.pdf ]
We define a coinductive semantics for a simple Javalike language by simply interpreting coinductively the rules of a standard bigstep operational semantics. We prove that such a semantics is sound w.r.t. the usual smallstep 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 smallstep 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 bigstep operational semantics and type systems.

[25] 
V. Mascardi and D Ancona.
1000 years of cooBDI.
In Declarative Agent Languages and Technologies IX 
9th International Workshop, DALT 2011, Revised Selected and Invited
Papers, pages 95101, 2011.
[ bib 
.pdf ]
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, CooBDI, 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 speechact based communication, including primitives for plan exchange. Besides allowing a natural and seamless integration with speechact based communication for BDI languages, the intuitions behind CooBDI 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 CooBDI and we outline other potential developments for future research.

[26] 
V. Mascardi, D. Ancona, R. H. Bordini, and A. Ricci.
CoolAgentSpeak: Enhancing AgentSpeakDL Agents with
Plan Exchange and Ontology Services.
In Proceedings of the 2011 IEEE/WIC/ACM International
Conference on Intelligent Agent Technology, IAT 2011, pages
109116, 2011.
[ bib 
.pdf ]
In this paper we present CooLAgentSpeak, an extension of AgentSpeakDL with plan exchange and ontology services. In CooLAgentSpeak, 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.

[27] 
D. Ancona and G. Lagorio.
On sound and complete axiomatization of coinductive subtyping for
objectoriented languages.
Technical report, DISI, November 2010.
Submitted for journal publication. Extended version of
FTfJP10.
[ bib 
.pdf ]
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.

[28] 
D. Ancona, A. Corradi, G. Lagorio, and F. Damiani.
Abstract compilation of objectoriented languages into coinductive
CLP(X): can type inference meet verification? (extended version).
Technical report, DISI, August 2010.
Extended version of
FoVeOOS10.
[ bib 
.pdf ]
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 Javalike 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 userdefined predicates, and propose an implementation based on a Prolog prototype metainterpreter, parametric in the solver for the subtyping constraints.

[29] 
D. Ancona and G. Lagorio.
Complete coinductive subtyping for abstract compilation of
objectoriented languages.
In FTFJP '10: Proceedings of the 12th Workshop on Formal
Techniques for JavaLike Programs, ACM Digital Library, pages
1:11:7. ACM, 2010.
[ bib 
.pdf 
http ]
Coinductive abstract compilation is a novel technique, which has been recently introduced, for defining precise type systems for objectoriented 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.

[30] 
D. Ancona and G. Lagorio.
Coinductive subtyping for abstract compilation of objectoriented
languages into Horn formulas.
In Montanari A., Napoli M., and Parente M., editors,
Proceedings of GandALF 2010, volume 25 of Electronic Proceedings in
Theoretical Computer Science, pages 214223, 2010.
[ bib 
.pdf ]
In recent work we have shown how it is possible to define very precise type systems for objectoriented 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.

[31] 
D. Ancona, A. Corradi, G. Lagorio, and F. Damiani.
Abstract compilation of objectoriented languages into coinductive
CLP(X): when type inference meets verification.
Technical report, Karlsruhe Institute of Technology, 2010.
Formal Verification of ObjectOriented Software. Papers
presented at the International Conference, June 2830, 2010, Paris,
France.
[ bib 
.pdf ]
We propose a novel general approach for defining expressive type systems for objectoriented 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.

[32] 
D. Ancona and V. Mascardi.
Exploiting Agents and Ontologies for Type and MeaningSafe
Adaptation of Java Programs.
In Proceedings of the MALLOWAWESOME 2009 workshop, volume
494. CEUR Workshop Proceedings, 2009.
[ bib 
.pdf ]
This paper discusses an application of intelligent software agents and ontologies to solve the problem of semiautomatic porting of Java programs. We have designed a system for aiding users to adapt Java code in a type and meaningsafe 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 typetheoretic notions of subtyping and type isomorphism with ontology matching. While the former notions are needed to ensure flexible adaptation in the presence of typesafety, 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 semiautomatic porting service he/she required.

[33] 
A. Cuni, D. Ancona, and A. Rigo.
Faster than C#: efficient implementation of dynamic languages on
.NET.
In ICOOOLPS '09: Proceedings of the 4th workshop on the
Implementation, Compilation, Optimization of ObjectOriented
Languages and Programming Systems, pages 2633, New York, NY, USA,
2009. ACM.
[ bib 
DOI 
.pdf ]
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 twolayers 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.

[34] 
D. Ancona, G. Lagorio, and E. Zucca.
Type inference by coinductive logic programming.
In de' Liguoro U. Berardi S., Damiani F., editor,
PostProceedings of TYPES 2008, volume 5497 of Lecture Notes in
Computer Science. Springer Verlag, 2009.
[ bib 
.pdf ]
We propose a novel approach to constraintbased 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 objectoriented 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 objectoriented 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.

[35] 
D. Ancona and G. Lagorio.
Coinductive type systems for objectoriented languages.
In S. Drossopoulou, editor, ECOOP 2009  ObjectOriented
Programming, volume 5653 of Lecture Notes in Computer Science, pages
226. Springer Verlag, 2009.
Best paper prize.
[ bib 
.pdf ]
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 objectoriented 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 objectoriented 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.

This file was generated by bibtex2html 1.98.