Davide Ancona's conference and workshop papers

[1] D. Ancona, F. Dagnino, and E. Zucca. Generalizing inference systems by coaxioms. In European Symposium on Programming, ESOP 2016, 2017. To appear. [ bib | .pdf ]
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.

[2] D. Ancona, A. Ferrando, and V. Mascardi. Comparing trace expressions and linear temporal logic for runtime verification. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 47--64, 2016. [ bib | .pdf ]
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.

[3] D. Ancona and A. Corradi. A formal account of ssa in java-like languages. In Proceedings of the 18th Workshop on Formal Techniques for Java-like Programs, FTfJP'16, pages 2:1--2:8. ACM, 2016. [ bib ]
[4] D. Ancona and A. Corradi. Semantic subtyping for imperative object-oriented languages. In OOPSLA 2016, pages 568--587, 2016. [ bib ]
[5] Davide Ancona, Daniela Briola, Amal El Fallah-Seghrouchni, 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 16-18, 2014., pages 30--45, 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 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.

[6] 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 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 62--73. 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.

[7] D. Ancona and A. Corradi. Sound and complete subtyping between coinductive types for object-oriented languages. In ECOOP 2014 - Object-Oriented 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.

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.

[8] D. Ancona. How to Prove Type Soundness of Java-like Languages Without Forgoing Big-step Semantics. In Formal techniques for Java-like programs (FTfJP14), pages 1:1--1:6. ACM, 2014. [ bib | .pdf ]
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.

[9] 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 3-5, 2014, pages 81--91, 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 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.

[10] D. Ancona, M. Barbieri, and V. Mascardi. Constrained Global Types for Dynamic Checking of Protocol Conformance in Multi-Agent Systems. In ACM Symposium on Applied Computing (SAC 2013), pages 1--3, 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.

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”.

[11] D. Ancona and E. Zucca. Safe Corecursion in coFJ. In Formal techniques for Java-like programs (FTfJP13), pages 2:1--2:7, 2013. [ bib | .pdf ]
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.

[12] D. Ancona, P. Giannini, and E. Zucca. Reconciling positional and nominal binding. In Intersection Types and Related Systems (ITRS 2013), pages 81--93, 2013. [ bib | .pdf ]
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.

[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 4-6, 2013. Proceedings, pages 300--311, 2013. [ bib | .pdf ]
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.

[14] D. Ancona, V. Mascardi, and O. Pavarino. Ontology-based documentation extraction for semi-automatic migration of Java code. In S. Ossowski and P. Lecca, editors, ACM Symposium on Applied Computing (SAC 2012), pages 1137--1143. 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 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.

[15] D. Ancona. Regular corecursion in Prolog. In S. Ossowski and P. Lecca, editors, ACM Symposium on Applied Computing (SAC 2012), pages 1897--1902, 2012. [ bib | .pdf ]
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.

[16] D. Ancona. Soundness of Object-Oriented Languages with Coinductive Big-Step Semantics. In J. Noble, editor, ECOOP 2012 - Object-Oriented Programming, volume 7313, pages 459--483. Springer, 2012. [ bib | .pdf ]
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.

[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 10--27. 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 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.

[18] D. Ancona and E. Zucca. Translating corecursive Featherweight Java in coinductive logic programming. In Co-LP 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 Multi-Agent Systems (Extended Abstract). In P. Massazza, editor, 13th Italian Conference on Theoretical Computer Science (ICTCS 2012), pages 39--43, 2012. [ bib | .pdf ]
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'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 Java-like programs (FTfJP12), 2012. [ bib | .pdf ]
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.

[21] D. Ancona, S. Drossopoulou, and V. Mascardi. Automatic Generation of Self-Monitoring MASs from Multiparty Global Session Types in Jason. In Declarative agent languages and technologies (DALT 2012)., pages 1--20. 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 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.

[22] D. Ancona, A. Corradi, G. Lagorio, and F. Damiani. Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification? In B. Beckert and C. Marché, editors, Formal Verification of Object-Oriented Software International Conference, FoVeOOS 2010, Paris, France, June 28-30, 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 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.

[23] D. Ancona. Coinductive big-step operational semantics for type soundness of Java-like languages. In Formal Techniques for Java-like Programs (FTfJP11), pages 5:1--5:6. ACM, 2011. [ bib | .pdf ]
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.

[24] V. Mascardi and D Ancona. 1000 years of coo-BDI. In Declarative Agent Languages and Technologies IX - 9th International Workshop, DALT 2011, Revised Selected and Invited Papers, pages 95--101, 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, 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.

[25] V. Mascardi, D. Ancona, R. H. Bordini, and A. Ricci. Cool-AgentSpeak: Enhancing AgentSpeak-DL Agents with Plan Exchange and Ontology Services. In Proceedings of the 2011 IEEE/WIC/ACM International Conference on Intelligent Agent Technology, IAT 2011, pages 109--116, 2011. [ bib | .pdf ]
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.

[26] D. Ancona and G. Lagorio. Complete coinductive subtyping for abstract compilation of object-oriented languages. In FTFJP '10: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, ACM Digital Library, pages 1:1--1:7. ACM, 2010. [ bib | .pdf | http ]
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.

[27] D. Ancona and G. Lagorio. Coinductive subtyping for abstract compilation of object-oriented 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 214--223, 2010. [ bib | .pdf ]
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.

[28] D. Ancona and V. Mascardi. Exploiting Agents and Ontologies for Type- and Meaning-Safe Adaptation of Java Programs. In Proceedings of the MALLOW-AWESOME 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 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.

[29] 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 Object-Oriented Languages and Programming Systems, pages 26--33, 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 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.

[30] D. Ancona, G. Lagorio, and E. Zucca. Type inference by coinductive logic programming. In de' Liguoro U. Berardi S., Damiani F., editor, Post-Proceedings of TYPES 2008, volume 5497 of Lecture Notes in Computer Science. Springer Verlag, 2009. [ bib | .pdf ]
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.

[31] D. Ancona and G. Lagorio. Coinductive type systems for object-oriented languages. In S. Drossopoulou, editor, ECOOP 2009 - Object-Oriented Programming, volume 5653 of Lecture Notes in Computer Science, pages 2--26. 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 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.

[32] D. Ancona, G. Lagorio, and E. Zucca. Type inference for polymorphic methods in Java-like languages. In G. Italiano, E. Moggi, and L. Laura, editors, Theoretical Computer Science: Proceedings of the 10th Italian Conference on ICTCS '07. World Scientific, 2007. See also the long version with proofs. [ bib | .pdf ]
In languages like C++, Java and C#, typechecking algorithms require methods to be annotated with their parameter and result types, which are either fixed or constrained by a bound. We show that, surprisingly enough, it is possible to infer the polymorphic type of a method where parameter and result types are left unspecified, as happens in most functional languages. These types intuitively capture the (less restrictive) requirements on arguments needed to safely apply the method. We formalize our ideas on a minimal Java subset, for which we define a type system with polymorphic types and prove its soundness. We then describe an algorithm for type inference and prove its soundness and completeness. A prototype implementing inference of polymorphic types is available.

[33] D. Ancona and E. Zucca. A formal framework for compositional compilation (extended abstract). In D. Ancona, G. Lagorio, and E. Zucca, editors, Theoretical Computer Science: Proceedings of the 10th Italian Conference on ICTCS '07. World Scientific, 2007. See also the long version with proofs and examples of framework instantiation. [ bib | .pdf ]
We define a general framework for compositional compilation, meant as the ability of building an executable application by separate compilation and linking of single fragments, opposed to global compilation of the complete source application code. More precisely, compilation of a source code fragment in isolation generates a corresponding binary fragment equipped with type information, formally modeled as a typing, allowing type safe linking of fragments without re-inspecting code. We formally define a notion of soundness and completeness of compositional compilation w.r.t. global compilation, and show how linking can be in practice expressed by an entailment relation on typings. Then, we provide a sufficient condition on such entailment to ensure soundness and completeness of compositional compilation, and compare this condition with the principal typings property. Furthermore, we show that this entailment relation can often be modularly expressed by an entailment relation on type environments and a subtyping relation.

[34] D. Ancona, M. Ancona, A Cuni, and N. Matsakis. RPython: a Step Towards Reconciling Dynamically and Statically Typed OO Languages. In OOPSLA 2007 Proceedings and Companion, DLS'07: Proceedings of the 2007 Symposium on Dynamic Languages, pages 53--64. ACM, 2007. [ bib | .pdf ]
Although the C-based interpreter of Python is reasonably fast, implementations on the CLI or the JVM platforms offers some advantages in terms of robustness and interoperability. Unfortunately, because the CLI and JVM are primarily designed to execute statically typed, object-oriented languages, most dynamic language implementations cannot use the native bytecodes for common operations like method calls and exception handling; as a result, they are not able to take full advantage of the power offered by the CLI and JVM. We describe a different approach that attempts to preserve the flexibility of Python, while still allowing for efficient execution. This is achieved by limiting the use of the more dynamic features of Python to an initial, bootstrapping phase. This phase is used to construct a final RPython (Restricted Python) program that is actually executed. RPython is a proper subset of Python, is statically typed, and does not allow dynamic modification of class or method definitions; however, it can still take advantage of Python features such as mixins and first-class methods and classes. This paper presents an overview of RPython, including its design and its translation to both CLI and JVM bytecode. We show how the bootstrapping phase can be used to implement advanced features, like extensible classes and generative programming. We also discuss what work remains before RPython is truly ready for general use, and compare the performance of RPython with that of other approaches.

[35] D. Ancona, G. Lagorio, and E. Zucca. Flexible type-safe linking of components for Java-like languages. In Joint Modular Languages Conference (JMLC 2006), volume 4228 of Lecture Notes in Computer Science, pages 136--154. Springer Verlag, 2006. See also the extended version. [ bib | .pdf ]
We define a framework of components based on Java-like languages, where components are binary mixin modules. Basic components can be obtained from a collection of classes by compiling such classes in isolation; for allowing that, requirements in the form of type constraints are associated with each class. Requirements are specified by the user who, however, is assisted by the compiler which can generate missing constraints essential to guarantee type safety. Basic components can be composed together by using a set of expressive typed operators; thanks to soundness results, such a composition is always type safe. The framework is designed as a separate layer which can be instantiated on top of any Java-like language; a prototype implementation is available for a small Java subset. Besides safety, the approach achieves great flexibility in reusing components for two reasons: (1) type constraints generated for a single component exactly capture all possible contexts where it can be safely used; (2) composition of components is not limited to conventional linking, but is achieved by means of a set of powerful operators typical of mixin modules.

[36] D. Ancona, G. Lagorio, and E. Zucca. Smart modules for Java-like languages. In 7th Intl. Workshop on Formal Techniques for Java-like Programs 2005, July 2005. [ bib | .pdf ]
We present SmartJavaMod, a language of mixin modules supporting compositional compilation, and constructed on top of the Java language. More in detail, this means that basic modules are collections of Java classes which can be typechecked in isolation, inferring constraints on missing classes and allowing safe reuse of the module in as many contexts as possible. Furthermore, it is possible to write structured module expressions by means of a set of module operators, and a type system at the module level ensures type safety, in the sense that we can always reduce a module expression to a well-formed collection of Java classes. What we obtain is a module language which is extremely flexible and allows the encoding (without any need of enriching the core level, that is, the Java language) of a variety of constructs supporting software reuse and extensibility.

[37] V. Mascardi, D. Demergasso, and D. Ancona. Languages for Programming BDI-style Agents: an Overview. In F. Corradini, F. De Paoli, E. Merelli, and A. Omicini, editors, WOA 2005 - Workshop From Objects to Agents, pages 9--15, 2005. [ bib | .pdf ]
The notion of an intelligent agent as an entity which appears to be the subject of mental attitudes like beliefs, desires and intentions (hence, the BDI acronym) is well known and accepted by many researchers. Besides the definition of various BDI logics, many languages and integrated environments for programming BDI-style agents have been proposed since the early nineties. In this reasoned bibliography, nine languages and implemented systems, namely PRS, dMARS, JACK, JAM, Jadex, AgentSpeak(L), 3APL, Dribble, and Coo-BDI, are discussed and compared. References to other systems and languages based on the BDI model are also provided, as well as pointers to surveys dealing with related topics.

[38] D. Ancona, F. Damiani, S. Drossopoulou, and E. Zucca. Polymorphic bytecode: Compositional compilation for Java-like languages. In POPL 2005 - The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 26--37. ACM Press, 2005. [ bib | .pdf ]
We define compositional compilation as the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but also depends on the compilation context. We propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard) bytecode that can be obtained by replacing type variables with classes satisfying the associated constraints. We illustrate our proposal by developing a typing and a linking algorithm. The typing algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment and constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, linking a self-contained collection of fragments either fails, or produces standard bytecode (the same as what would have been produced by standard compilation of all fragments).

[39] D. Ancona, S. Fagorzi, and E. Zucca. Mixin modules for dynamic rebinding. In R. De Nicola and D. Sangiorgi, editors, Trustworthy Global Computing: IST/FET International Workshop, TGC 2005, Edinburgh, UK, April 7-9, 2005. Revised Selected Papers, volume 3705 of Lecture Notes in Computer Science, pages 279--298. Springer Verlag, 2005. [ bib | .pdf ]
Dynamic rebinding is the ability of changing the definitions of names at execution time. While dynamic rebinding is clearly useful in practice, and increasingly needed in modern systems, most programming languages provide only limited and ad-hoc mechanisms, and no adequate semantic understanding currently exists. Here, we provide a simple and powerful mechanism for dynamic rebinding by means of a calculus of mixin modules (mutually recursive modules allowing redefinition of components) where, differently from the traditional approach, module operations can be performed after selecting and executing a module component: in this way, execution can refer to virtual components, which can be rebound when module operators are executed. In particular, in our calculus module operations are performed on demand, when execution would otherwise get stuck. We provide a sound type system, which ensures that execution never tries to access module components which cannot become available, and show how the calculus can be used to encode a variety of real-world dynamic rebinding mechanisms.

[40] L. Bozzo, V. Mascardi, D. Ancona, and P. Busetta. COOWS: Adaptive BDI Agents meet Service-Oriented Computing. In M. P. Gleizes, G. A. Kaminka, A. Nowé, S. Ossowski, K. Tuyls, and K. Verbeeck, editors, EUMAS 2005 - Proceedings of the Third European Workshop on Multi-Agent Systems, Brussels, Belgium, December 7-8, 2005, page 473, 2005. [ bib | http ]
Mainstream research in Web Services is currently looking at two main aspects, namely formally describing interactions among services, and finding and combining services. Much work made in the intelligent agents area is being applied to these issues. In this paper, we investigate the application of agent research to Web Services from a different perspective, that is, procedural learning. The final objective is to enable an adaptive system (an agent in our terminology) to discover or being fed with knowledge concerning how to solve a specific set of problems in a specific software or physical environment. Our work is a very preliminary step into the issue, with the main objective of assessing how current Web Services technology can support a component, described in terms of beliefs, desires and intentions, dynamically adapting its behaviour to new environments.

[41] D. Ancona and E. Moggi. Program Generation and Components. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. de Roever, editors, Formal Methods for Components and Objects: Third International Symposium, FMCO 2004, volume 3657 of Lecture Notes in Computer Science, pages 222--250. Springer Verlag, 2005. [ bib | .pdf ]
The first part of the paper gives a brief overview of meta-programming, in particular program generation, and its use in software development. The second part introduces a basic calculus, related to FreshML, that supports program generation (as described through examples and a translation of MetaML into it) and programming in-the-large (this is demonstrated by a translation of CMS into it).

[42] D. Ancona, F. Damiani, S. Drossopoulou, and E. Zucca. Even more principal typings for Java-like languages. In 6th Intl. Workshop on Formal Techniques for Java Programs 2004, June 2004. [ bib | .pdf ]
We propose an innovative type system for Java-like languages which can infer the minimal set of assumptions guaranteeing type correctness of a class c, and generate (abstract) bytecode for c, by inspecting the source code of c in isolation. We prove the above properties of our type system by showing that it has principal typings. As well known, principal typings support compositional analysis, whereby a collection of classes can be safely linked together without further inspection of the classes' code, provided that each class has been typechecked in isolation (intra-checking), and that the mutual class assumptions are satisfied (inter-checking). We also develop an algorithm for inter-checking, and prove it correct.

[43] D. Ancona and E. Moggi. A Fresh Calculus for Name Management. In G. Karsai and E. Visser, editors, Generative Programming and Component Engineering (GPCE 2004), volume 3286 of Lecture Notes in Computer Science, pages 206--224. Springer Verlag, 2004. [ bib | .pdf ]
We define a basic calculus for name management, which is obtained by an appropriate combination of three ingredients: extensible records (in a simplified form), names (as in FreshML), computational types (to allow computational effects, including generation of fresh names). The calculus supports the use of symbolic names for programming in-the-large, e.g. it subsumes Ancona and Zucca's calculus for module systems, and for meta-programming (but not the intensional analysis of object level terms supported by FreshML), e.g. it subsumes (and improves) Nanevski and Pfenning's calculus for meta-programming with names and necessity. Moreover, it models some aspects of Java's class loaders.

[44] S. Fagorzi, E. Zucca, and D. Ancona. Modeling multiple class loaders by a calculus for dynamic linking. In H. Haddad, A. Omicini, R. L. Wainwright, and L. M. Liebrock, editors, SAC 2004 - Proceedings of the 2004 ACM Symposium on Applied Computing, pages 1281--1288. ACM Press, 2004. [ bib | .ps.gz ]
A recent paper proposes a calculus for modeling dynamic linking independently of the details of a particular programming environment. Here we use a particular instantiation of this calculus to encode a toy language, called MCL, which provides an abstract view of the mechanism of dynamic class loading with multiple loaders as in Java. The aim is twofold. On one hand, we show the effectiveness of the calculus in modeling existing loading and linking policies. On the other hand, we provide a simple formal model which allows a better understanding of Java-like loading mechanisms and also shows an intermediate solution between the rigid approach based only on the classpath and that which allows arbitrary user-defined loaders, which can be intricate and error-prone.

[45] D. Ancona and E. Zucca. Principal typings for Java-like languages. In POPL 2004 - The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 306--317. ACM Press, 2004. [ bib | .ps.gz ]
The contribution of the paper is twofold. First, we provide a general notion of type system supporting separate compilation and inter-checking, and a formal definition of soundess and completeness of inter-checking w.r.t. global compilation. These properties are important in practice since they allow selective recompilation. In particular, we show that they are guaranteed when the type system has principal typings and provides sound and complete entailment relation between type environments and types. The second contribution is more specific, and is an instantiation of the notion of type system previously defined for Featherweight Java [IgarashiEtAl99] with method overloading and field hiding. The aim is to show that it is possible to define type systems for Java-like languages, which, differently from those used by standard compilers, have principal typings, hence can be used as a basis for selective recompilation.

[46] D. Ancona, S. Fagorzi, and E. Zucca. A calculus with lazy module operators. In J.-J. Levy, E. W. Mayr, and J. C. Mitchell, editors, IFIP 18th World Computer Congress, TC1 3rd Int. Conf. on Theoretical Computer Science (TCS2004), pages 423--436. Kluwer Academic Publishers, 2004. [ bib | .pdf ]
Modern programming environments such as those of Java and C# support dynamic loading of software fragments. More in general, we can expect that in the future systems will support more and more forms of interleaving of reconfiguration steps and standard execution steps, where the software fragments composing a program are dynamically changed and/or combined on demand and in different ways. However, existing kernel calculi providing formal foundations for module systems are based on a static view of module manipulation, in the sense that open code fragments can be flexibly combined together, but all module operators must be performed once for all before starting execution of a program, that is, evaluation of a module component. The definition of clean and powerful module calculi supporting lazy module operators, that is, operators which can be performed after the selection of some module component, is still an open problem. Here, we provide an example in this direction (the first at our knowledge), defining DCMS, an extension of the Calculus of Module Systems where module operators can be performed at execution time and, in particular, are executed on demand, that is, only when needed by the executing program. In other words, execution steps, if possible, take the precedence over reconfiguration steps. The type system of the calculus, which is proved to be sound, relies on a dependency analysis which ensures that execution will never try to access module components which cannot become available by performing reconfiguration steps.

[47] D. Ancona, V. Mascardi, J.F. Hübner, and R. H. Bordini. Coo-AgentSpeak: Cooperation in AgentSpeak through Plan Exchange. In N. R. Jennings, C. Sierra, L. Sonenberg, and M. Tambe, editors, AAMAS 2004 (Int. Conf. on Autonomous Agents and Multiagent Systems), pages 698--705. ACM press, 2004. [ bib | .pdf ]
This paper brings together two recent contributions to the area of declarative agent-oriented programming, made feasible in practice by the recent introduction of an interpreter for a BDI programming language. The work on CooBDI has proposed an approach to plan exchange which applies to BDI agents in general. The other contribution is the introduction of special illocutionary forces for plan exchange between AgentSpeak agents. This has been implemented in Jason, an interpreter for an extended version of AgentSpeak(L). Jason also provides mechanisms that allow the specification of plan permissions, which are important in the cooperation context. This paper shows how elaborate plan exchange can take place between AgentSpeak agents implemented with Jason. It also discusses an application in which plan sharing is essential.

[48] D. Ancona and V. Mascardi. Coo-BDI: Extending the BDI Model with Cooperativity. In J. Leite, A. Omicini, L. Sterling, and P. Torroni, editors, Declarative Agent Languages and Techniques, First International Workshop, DALT 2003, Revised Selected and Invited Papers, volume 2990 of Lecture Notes in Computer Science, pages 109--134. Springer Verlag, 2004. [ bib | .ps.gz ]
We define Coo-BDI, an extension of the BDI architecture with the notion of cooperativity. Agents can cooperate by exchanging and sharing plans in a quite flexible way. As a main result Coo-BDI promotes adaptivity and sharing of resources; as a by-product, it provides a better support for dealing with agents which do not possess their own procedural knowledge for processing a given event.

[49] D. Ancona, S. Fagorzi, E. Moggi, and E. Zucca. Mixin modules and computational effects. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, ICALP 2003 - Automata, Languages and Programming, volume 2719 of Lecture Notes in Computer Science, pages 224--238. Springer Verlag, 2003. [ bib | .ps.gz ]
We define a calculus for investigating the interactions between mixin modules and computational effects, by combining the purely functional mixin calculus CMS with a monadic metalanguage supporting the two separate notions of simplification (local rewrite rules) and computation (global evaluation able to modify the store). This distinction is important for smoothly integrating the CMS rules (which are all local) with the rules dealing with the imperative features. In our calculus mixins can contain mutually recursive computational components which are explicitly computed by means of a new mixin operator whose semantics is defined in terms of a Haskell-like recursive monadic binding. Since we mainly focus on the operational aspects, we adopt a simple type system like that for Haskell, that does not detect dynamic errors related to bad recursive declarations involving effects. The calculus serves as a formal basis for defining the semantics of imperative programming languages supporting first class mixins while preserving the CMS equational reasoning.

[50] D. Ancona and G. Lagorio. Stronger typings for separate compilation of Java-like languages (Extended Abstract). In 5th Intl. Workshop on Formal Techniques for Java Programs 2003, 2003. [ bib | .ps.gz | http | .html ]
We define and implement a formal system supporting separate compilation for a small but significant Java-like language. This system is proved to be stronger than the standard compilation of both Java and C#, in the sense that it better supports software reuse by avoiding unnecessary recompilation steps after code modification which are usually performed by using the standard compilers. This is achieved by introducing the notion of local type assumption allowing the user to specify weaker requirements on the source fragments which need to be compiled in isolation. Another important property satisfied by our system is compositionality, which corresponds to the intuition that if a set of fragments can be separately compiled and such fragments are compatible, then it is possible to compile all the fragments together as a unique program and obtain the same result.

[51] D. Ancona, S. Fagorzi, and E. Zucca. A calculus for dynamic linking. In C. Blundo and C. Laneve, editors, ICTCS 2003 - Theoretical Computer Science, volume 2841 of Lecture Notes in Computer Science, pages 284--301. Springer Verlag, 2003. [ bib | .ps.gz ]
We define a calculus for modeling dynamic linking independently of the details of a particular programming environment. The calculus distinguishes at the language level the notions of software configuration and execution, by introducing separate syntactic notions of linkset expression and command, respectively. A reduction step can be either a simplification of a linkset expression, or the execution of a command w.r.t. a specific underlying software configuration denoted by a linkset expression; because of dynamic linking, these two kinds of reductions are interleaved. The type system of the calculus, which is proved to be sound, relies on an accurate dependency analysis for ensuring type safety without losing the advantages offered by dynamic linking.

[52] D. Ancona, G. Lagorio, and E. Zucca. True separate compilation of Java classes. In ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02), pages 189--200. ACM Press, 2002. [ bib | .ps.gz ]
We define a type system modeling true separate compilation for a small but significant Java subset, in the sense that a single class declaration can be intra-checked (following the Cardelli's terminology) and compiled providing a minimal set of type requirements on missing classes. These requirements are specified by a local type environment associated with each single class, while in the existing formal definitions of the Java type system classes are typed in a global type environment containing all the type information on a closed program. We also provide formal rules for static inter-checking and relate our approach with compilation of closed programs, by proving that we get the same results.

[53] D. Ancona, G. Lagorio, and E. Zucca. A formal framework for Java separate compilation. In B. Magnusson, editor, ECOOP 2002 - Object-Oriented Programming, volume 2374 of Lecture Notes in Computer Science, pages 609--635. Springer Verlag, 2002. [ bib | .ps.gz ]
We define a formal notion, called compilation schema, allowing to specify different possibilities for performing the overall process of Java compilation, which includes type-checking of source fragments with generation of corresponding binary code, type-checking of binary fragments, extraction of type information from fragments and definition of dependencies among them. We consider three compilation schemata of interest for Java, that is, minimal, SDK and safe, which correspond to a minimal set of checks, the checks performed by the SDK implementation, and all the checks needed to prevent run-time linkage errors, respectively. In order to demonstrate our approach, we define a kernel model for Java separate compilation and execution, consisting in a small Java subset, and a simple corresponding binary language for which we provide an operational semantics including run-time verification. We define a safe compilation schema for this language and formally prove type safety.

[54] D. Ancona and E. Zucca. True modules for Java-like languages. In J.L. Knudsen, editor, ECOOP 2001 - Object-Oriented Programming, volume 2072 of Lecture Notes in Computer Science, pages 354--380. Springer Verlag, 2001. [ bib | .ps.gz ]
We present JavaMod, a true module system constructed on top of a Java-like language. More in detail, this means that basic modules are collections of Java classes and specify in their interface the imported and exported classes with their types; furthermore, it is possible to write structured module expressions by means of a set of module operators and a type system at the module level ensures type safety. In designing such a type system, one has to face non trivial problems, notably the fact that a module M which extends an imported class C can be correctly combined only with modules exporting a class C which, besides providing the expected services, causes no interferences with its subclasses defined in M. What we obtain is a module language which is extremely flexible and allows to express (without any need of enriching the syntax of the core level, that is, the Java language), for instance, generic types as in Pizza and GJ, mixin classes (that is, subclasses parametric in the direct superclass) and mutually recursive class definitions split in independent modules.

[55] D. Ancona, G. Lagorio, and E. Zucca. Java separate type checking is not safe. In 3rd Intl. Workshop on Formal Techniques for Java Programs 2001, 2001. [ bib | .ps.gz | http ]
Java supports separate type-checking in the sense that compilation can be invoked on a single source fragment, and this may enforce type-checking of other either source or binary fragments existing in the environment. However, the Java specification does not define precise rules on how this process should be performed, therefore the outcome of compilation may strongly depend on the particular compiler implementation. Furthermore, rules adopted by standard Java compilers, as SDK and Jikes, can produce binary fragments whose execution throws linking related errors. We introduce a simple framework which allows to formally express the process of separate compilation and the related formal notion of type safety. Moreover, we define, for a small subset of Java, a type system for separate compilation which we conjecture to be safe.

[56] D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini, and E. Zucca. An effective translation of Fickle into Java. In A. Restivo, S. Ronchi Della Rocca, and L. Roversi, editors, ICTCS 2001 - Theoretical Computer Science, volume 2202 of Lecture Notes in Computer Science, pages 215--234. Springer Verlag, 2001. [ bib | .ps.gz ]
We present a translation from Fickle (a Java-like language allowing dynamic object re-classification, that is, objects that can change their class at run-time) into plain Java. The translation is proved to preserve static and dynamic semantics; moreover, it is shown to be effective, in the sense that the translation of a Fickle class does not depend on the implementation of used classes, hence can be done in a separate way, that is, without having their sources, exactly as it happens for Java compilation. The aim is to demonstrate that an extension of Java supporting dynamic object re-classification could be fully compatible with the existing Java environment.

[57] D. Ancona, G. Lagorio, and E. Zucca. A core calculus for Java exceptions. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2001), SIGPLAN Notices. ACM Press, 2001. [ bib | .ps.gz ]
In this paper we present a simple calculus (called CJE) in order to fully investigate the exception mechanism of Java, and in particular its interaction with inheritance, which turns out to be non trivial. Moreover, we show that the type system for the calculus directly driven by the Java Language Specification (called FULL) uses too many types, in the sense that there are different types which provide exactly the same information. Hence, we obtain from FULL a simplified type system called MIN where equivalent types have been identified. We show that this is useful both for type-checking optimization and for clarifying the static semantics of the language. The two type systems are proved to satisfy the subject reduction property.

[58] D. Ancona, E. Zucca, and S. Drossopoulou. Overloading and inheritance. In The Eighth International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001. [ bib | .ps.gz ]
Overloading allows several function definitions for the same name, distinguished primarily through different argument types; it is typically resolved at compile-time. Inheritance allows subclasses to define more special versions of the same function; it is typically resolved at run-time. Modern object-oriented languages incorporate both features, usually in a type-safe manner. However, the combination of these features sometimes turns out to have surprising, and even counterintuitive, effects. We discuss why we consider these effects inappropriate, and suggest alternatives. We explore the design space by isolating the main issues involved and analyzing their interplay and suggest a formal framework describing static overloading resolution and dynamic function selection, abstracting from other language features. We believe that our framework clarifies the thought process going on at language design level. We introduce a notion of soundness and completeness of an overloading resolution policy w.r.t. the underlying dynamic semantics, and a way of comparing the flexibility of different resolution policies. We apply these concepts to some non-trivial issues raised in concrete languages. We also argue that the semantics of overloading and inheritance is “clean” only if it can be understood through a copy semantics, whereby programs are transformed to equivalent programs without subclasses, and the effect of inheritance is obtained through copying.

[59] D. Ancona, G. Lagorio, and E. Zucca. Jam: A smooth extension of Java with mixins. In E. Bertino, editor, ECOOP 2000 - Object-Oriented Programming, volume 1850 of Lecture Notes in Computer Science, pages 154--178. Springer Verlag, 2000. [ bib | .ps.gz | http ]
In this paper we present Jam, an extension of the Java language supporting mixins, also called parametric heir classes. A mixin declaration in Jam is similar to a Java heir class declaration, apart that mixins do not extend a fixed parent class, but simply specify the set of fields and methods a generic parent should provide. In this way, the same mixin can be instantiated on many parent classes, producing different heir classes, thus avoiding code duplication and largely improving modularity and reuse. Moreover, as happens for classes and interfaces, mixin names are reference types, and all the classes obtained instantiating the same mixin are considered subtypes of the corresponding type, hence can be handled in a uniform way through the common interface. This possibility allows a programming style where different ingredients are "mixed" together in defining a class; this paradigm is partly similar to that based on multiple inheritance, but avoids its complication. The language has been designed with the main objective in mind to obtain, rather than a new theoretical language, a working and smooth extension of Java. That means, on the design side, that we have faced the challenging problem of integrating the Java overall principles and complex type system with this new notion; on the implementation side, that we have developed a Jam to Java translator which makes Jam sources executable on every Java Virtual Machine.

[60] D. Ancona, G. Lagorio, and E. Zucca. A core calculus for Java exceptions (Extended Abstract). In 2nd Intl. Workshop on Formal Techniques for Java Programs 2000, 2000. [ bib | .pdf | http ]
In this paper we present a simple calculus (called CJE) corresponding to a small functional fragment of Java supporting exceptions. We provide a reduction semantics for the calculus together with two equivalent type systems; the former corresponds to the standard specication and its formalization, whereas the latter can be considered an optimization of the former where only the minimal type information about classes/interfaces and methods are collected in order to type-check a program. The two type systems are proved to be equivalent and a subject reduction theorem is given.

[61] D. Ancona, E. Zucca, and S. Drossopoulou. Overloading and inheritance in Java (Extended Abstract). In 2nd Intl. Workshop on Formal Techniques for Java Programs 2000, 2000. [ bib | .pdf | http ]
The combination of overloading and inheritance in Java introduces questions about function selection, and makes some function calls ambiguous. We believe that the approach taken by Java designers is counterintuitive. We explore an alternative, and argue that it is more intuitive and agrees with the Java rules for the cases where Java considers the function calls unambiguous, but gives meaning to more calls than Java does.

[62] D. Ancona and V. Mascardi. Mixin-based modules for logic programming. In APPIA-GULP-PRODE 2000. 2000 Joint Conference on Declarative Programming, 2000. [ bib | .ps.gz ]
In this paper we show how it is possible to define a rather rich language of mixin modules suitable for combining together large logic programs without changing the underlying logic. The type and reduction rules for the language are presented in a somehow informal way, whereas more emphasis is given to the usefulness of the constructs from the programming point of view and to the comparison with other proposals for modular logic programming found in the literature.

[63] D. Ancona, M. Cerioli, and E. Zucca. Extending Casl with late binding. In D. Bert and C. Choppy, editors, WADT'99 - 14th Workshop on Algebraic Development Techniques - Selected Papers, volume 1827 of Lecture Notes in Computer Science, pages 53--72. Springer Verlag, 2000. [ bib | .ps.gz ]
We define an extension of CASL, the standard language for algebraic specification, with a late binding mechanism. More precisely, we introduce a special kind of functions called methods, for which, differently to what happens for usual functions, overloading resolution is delayed at evaluation time and not required to be conservative. The extension consists, at the semantic level, in the definition of an institution LB supporting late binding which is defined on top of the standard subsorted institution of CASL and, at the linguistic level, in the enrichment of the CASL language with appropriate constructs for dealing with methods.

[64] D. Ancona. MIX(FL): a kernel language of mixin modules. In T. Rus, editor, AMAST 2000 - Algebraic Methodology and Software Technology, volume 1816 of Lecture Notes in Computer Science, pages 454--468. Springer Verlag, 2000. [ bib | .ps.gz ]
We define the language of mixin modules MIX(FL) with the aim of providing foundations for the design of module systems supporting mixins. Several working examples are presented showing the benefits of the use of mixins and overriding in module systems. The language is strongly typed and supports separate compilation. The denotational semantics of the language is based on an algebraic approach and is parametric in the semantics of the underlying core language. Hence, even though the language is defined on top of a specific core language, other kinds of core languages could be considered as well.

[65] D. Ancona and E. Zucca. A primitive calculus for module systems. In G. Nadathur, editor, PPDP'99 - International Conference of Principles and Practice of Declarative Programming, volume 1702 of Lecture Notes in Computer Science, pages 62--79. Springer Verlag, 1999. [ bib | .ps.gz | .html ]
We present a simple and powerful calculus of modules supporting mutual recursion and higher order features. The calculus allows to encode a large variety of existing mechanisms for combining software components, including parameterized modules like ML functors, extension with overriding of object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. As usual, we first present an untyped version of our calculus and then a type system which is proved sound w.r.t. the reduction semantics; moreover we give a translation of other primitive calculi.

[66] D. Ancona, M. Cerioli, and E. Zucca. A formal framework with late binding. In J.-P. Finance, editor, FASE'99 - Fundamental Approaches to Software Engineering, volume 1577 of Lecture Notes in Computer Science, pages 30--44. Springer Verlag, 1999. [ bib | .ps.gz ]
We define a specification formalism (formally, an institution) which provides a notion of dynamic type (the type which is associated to a term by a particular evaluation) and late binding (the fact that the function version to be invoked in a function application depends on the dynamic type of one or more arguments). Hence, it constitutes a natural formal framework for modeling object-oriented and other dynamically-typed languages and a basis for adding to them a specification level. In this respect, the main novelty is the capability of writing axioms related to a given type which are not required to hold for subtypes, hence can be “overridden” in further refinements, thus lifting at the specification level the possibility of reusing code which is offered by the object-oriented approach.

[67] D. Ancona. An algebraic framework for separate type-checking. In J. Fiadeiro, editor, WADT'98 - 13th Workshop on Algebraic Development Techniques - Selected Papers, volume 1589 of Lecture Notes in Computer Science, pages 1--15. Springer Verlag, 1999. [ bib | .ps.gz ]
We address the problem of defining an algebraic framework for modularization supporting separate type-checking. In order to do that we introduce the notions of abstract type system and logic of constraints and we present a canonical construction of a model part, on top of a logic of constraints. This canonical construction works under reasonable assumptions on the underlying type system (e.g., soundness of the system). We show that the framework is suitable for defining the static and dynamic semantics of module languages, by giving a concrete example of construction on top of the type system of a simple typed module language. As a result, the subtyping relation between module interfaces is captured in a natural way by the notion of signature morphism.

[68] D. Ancona and E. Zucca. An algebra of mixin modules. In F. Parisi-Presicce, editor, WADT'97 - 12th Workshop on Algebraic Development Techniques - Selected Papers, volume 1376 of Lecture Notes in Computer Science, pages 92--106. Springer Verlag, 1998. [ bib | .ps.gz ]
Mixins are modules which may contain deferred components, i.e. components not defined in the module itself, and allow definitions to be overridden. We give an axiomatic definition of a set of operations for mixin combination, corresponding to a variety of constructs existing in programming languages (merge, hiding, overriding, functional composition, ...). In particular, we show that they can all be expressed in terms of three primitive operations (namely, sum, reduct and freeze), which are characterized by a small set of axioms. We show that the given axiomatization is sound w.r.t. to a model provided in some preceding work. Finally, we prove the existence of anormal form for mixin expressions.

[69] D. Ancona and E. Zucca. Overriding operators in a mixin-based framework. In H. Glaser, P. Hartel, and H. Kuchen, editors, PLILP '97 - 9th Intl. Symp. on Programming Languages, Implementations, Logics, and Programs, volume 1292 of Lecture Notes in Computer Science, pages 47--61. Springer Verlag, 1997. [ bib | .ps.gz ]
We show that many different overriding operators present in programming languages can be expressed, adopting a mixin-based framework, in terms of three basic operators. In particular we propose two orthogonal classifications: strong (the overridden definition is canceled) or weak (the overridden definition still remains significant, as in Smalltalk's super feature), and preferential (priority to one of the two arguments) or general. We formalize the relation between all these versions. Our analysis and results are not bound to a particular language, since they are formulated within an algebraic framework for mixin modules which can be instantiated over different core languages.

[70] D. Ancona and E. Zucca. An algebraic approach to mixins and modularity. In M. Hanus and M. Rodríguez-Artalejo, editors, ALP '96 - 5th Intl. Conf. on Algebraic and Logic Programming, volume 1139 of Lecture Notes in Computer Science, pages 179--193. Springer Verlag, 1996. [ bib | .ps.gz ]
We present an algebraic formalization of the notion of mixin module, i.e. a module where the definition of some components is deferred. Moreover, we define a set of basic operators for composing mixin modules, intended to be a kernel language with clean semantics in which to express more complex operators of existing modular languages, including variants of inheritance in object oriented programming. The semantics of the operators is given in an institution independent way, i.e. is parameterized on the semantic framework modeling features of the underlying core language.

[71] D. Ancona and E. Zucca. A formal framework for modules with state. In M. Wirsing and M. Nivat, editors, AMAST '96 - Algebraic Methodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 148--162. Springer Verlag, 1996. [ bib | .ps.gz ]
We present a module algebra interpreted in the model of dynamic data-types. A data-type with state, or dynamic data type, is a data type in which the interpretation of operation symbols is depending on the internal state, which may change during the time. We formalize the above notion by a new mathematical structure, called object structure. From the point of view of programming languages, an object structure is the overall semantic value (the denotation) of a software module in an imperative context: Ada packages, Modula-2 modules and objects of object based languages can be thought as syntactic counterparts of object structures. Thus a first result of our approach is an abstract and natural definition of the semantic value of a whole module. A further result that we want to achieve is this semantics to be truly compositional, i.e. operations of composing modules to be interpreted as operations of object structures at the semantic level. We illustrate that by giving syntax and semantics of a module language which is parametric in the concrete syntax used for defining methods and components of the state. The introduction of state makes necessary to review the semantics of classical operators as given in a standard algebraic setting. In particular, we introduce a distinction between the visible and the internal signature of an object structure, which is essential for defining a reduct operation, hence for modelling export/hiding operators. Composition of visible signatures must be propagated to internal signatures in order to keep unchanged hidden components modulo renaming; this corresponds to consider co-products of particular diagrams in the category of signatures.

[72] D. Ancona, E. Astesiano, and E. Zucca. Towards a classification of inheritance relations. In U.W. Lipeck and G. Koschorreck, editors, Proc. ISCORE '93 (International Workshop on Information Systems - Correctness and Reusability), number 01/93 in Informatik-Berichte, pages 90--113. Universitaet Hannover, 1993. [ bib | .ps.gz ]
We address the problem of providing a rigorous formal model for classes of objects and the variety of inheritance relations. Classes are modelled by a new structure, called d-oid, which corresponds to see objects as data with state. The approach we take is a rather abstract one and so we model representation independent configurations of an object system by algebras, object identities by so called tracking map, and method calls as transformations of algebras. Seeing classes as d-oids allows us to define a hierarchy of inheritance relations, modelled by relations between d-oids and corresponding to different liberty levels in redefining methods. The classification we present distinguish essentially three levels of inheritance: minimal, regular and conservative.


This file was generated by bibtex2html 1.98.


Back to the main page on Davide Ancona's papers

Please send suggestions and comments to:
Davide Ancona davide.ancona@unige.it

Last Updated: January 2017