[1] 
D. Ancona, P. Giannini, and E. Zucca.
Incremental rebinding with name polymorphism.
Electr. Notes Theor. Comput. Sci., 322:1934, 2016.
[ bib 
DOI 
.pdf 
http ]
We propose an extension with name variables of a calculus for incremental rebinding of code introduced in previous work. Names, which can be either constants or variables, are used as interface of fragments of code with free variables. Open code can be dynamically rebound by applying a rebinding, which is an association from names to terms. Rebinding is incremental, since rebindings can contain free variables as well, and can be manipulated by operators such as overriding and renaming. By using name variables, it is possible to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly enhancing expressivity. The type system is correspondingly extended by constrained namepolymorphic types, where simple inequality constraints prevent conflicts among parametric name interfaces.

[2] 
D. Ancona, V. Bono, M. Bravetti, J. Campos, G. Castagna, P. M. Deniélou,
S. J. Gay, N. Gesbert, E. Giachino, R. Hu, E. B. Johnsen, F. Martins,
V. Mascardi, F. Montesi, R. Neykova, N. Ng, L. Padovani, V.T. Vasconcelos,
and N. Yoshida.
Behavioral types in programming languages.
Foundations and Trends in Programming Languages,
3(23):95230, 2016.
[ bib 
DOI 
.pdf 
http ]
A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of largescale, communicationintensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.

[3] 
D. Ancona and A. 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.

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

[6] 
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.

[7] 
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.

[8] 
D. Ancona, S. Fagorzi, and E. Zucca.
A parametric calculus for mobile open code.
Electronic Notes in Theoretical Computer Science, 192(3):3 
22, 2008.
Proceedings of the Third International Workshop on Developments in
Computational Models (DCM 2007).
[ bib 
DOI 
.pdf 
http ]
We present a simple parametric calculus of processes which exchange open mobile code, that is, code which may contain free variables to be bound by the receiver's code. Type safety is ensured by a combination of static and dynamic checks. That is, internal consistency of each process is statically verified, by relying on local type assumptions on missing code; then, when code is sent from a process to another, a runtime check based on a subtyping relation ensures that it can be successfully received, without requiring reinspection of the code. In order to refuse communication in as few cases as possible, the runtime check accepts even mobile code which would be rejected if statically available, by automatically inserting coercions driven by the subtyping relation, as in the socalled Penn translation. The calculus is parametric in some ingredients which can vary depending on the specific language or system. Notably, we abstract away from the specific nature of the code to be exchanged, and of the static and dynamic checks. We formalize the notion of type safety in our general framework and provide sufficient conditions on the above ingredients which guarantee this property. We illustrate our approach on a simple lambdacalculus with records, where type safe exchange of mobile code is made problematic by conflicts due to components which were not explicitly required. In particular, we show that the standard coercion semantics given in the literature, with other aims, for this calculus, allows to detect and eliminate conflicts due to inner components, thus solving a problem which was left open in previous work on typesafe exchange of mobile code.

[9] 
D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini, and E. Zucca.
A Provenly Correct Translation of Fickle into Java.
ACM Transactions on Programming Languages and Systems, 29(2),
April 2007.
[ bib 
.pdf ]
We present a translation from Fickle, a small objectoriented language allowing objects to change their class at runtime, into Java. The translation is provenly correct in the sense that it preserves the static and dynamic semantics. Moreover, it is compatible with separate compilation, since the translation of a Fickle class does not depend on the implementation of used classes. Based on the formal system, we have developed an implementation. The translation turned out to be a more subtle problem than we expected. In this article, we discuss four possible approaches we considered for the design of the translation and to justify our choice, we present formally the translation and proof of preservation of the static and dynamic semantics, and discuss the prototype implementation. Moreover, we outline an alternative translation based on generics that avoids most of the casts (but not all) needed in the previous translation. The language Fickle has undergone and is still undergoing several phases of development. In this article we are discussing the translation of FickleII.

[10] 
D. Ancona, S. Fagorzi, and E. Zucca.
A calculus for dynamic reconfiguration with low priority linking.
Electronic Notes in Theoretical Computer Science. Proceedings of
the Second Workshop on Object Oriented Developments (WOOD 2004),
138(2):335, 2005.
[ bib 
.pdf 
http ]
Building on our previous work, we present a simple module calculus where execution steps of a module component can be interleaved with reconfiguration steps (that is, reductions at the module level), and where execution can partly control precedence between these reconfiguration steps. This is achieved by means of a low priority link operator which is only performed when a certain component, which has not been linked yet, is both available and really needed for execution to proceed, otherwise precedence is given to the outer operators. We illustrate the expressive power of this mechanism by a number of examples. We ensure soundness by combining a static type system, which prevents errors in applying module operators, and a dynamic check which raises a linkage error if the running program needs a component which cannot be provided by reconfiguration steps. In particular no linkage errors can be raised if all components are potentially available.

[11] 
D. Ancona and G. Lagorio.
Stronger Typings for Smarter Recompilation of Javalike
Languages.
Journal of Object Technology. Special issue. Workshop on Formal
Techniques for Javalike Programs (FTfJP) ECOOP 2003, 3(6):525, June 2004.
[ bib 
.ps.gz 
http 
http ]
We define an algorithm for smarter recompilation of a small but significant Javalike language; such an algorithm is inspired by a type system previously defined by Ancona and Zucca. In comparison with all previous type systems for Javalike languages, this system enjoys the principal typings property, and is based on the two novel notions of local type assumption and entailment of type environments. The former allows the user to specify minimal requirements on the source fragments which need to be compiled in isolation, whereas the latter syntactically captures the concept of stronger type assumption. One of the most important practical advantages of this system is a better support for selective recompilation; indeed, it is possible to define an algorithm directly driven by the typing rules which is able to avoid the unnecessary recompilation steps which are usually performed by the Java compilers. The algorithm is smarter in the sense that it never forces useless recompilations, that is, recompilations which would generate the same binary fragment obtained from the previous compilation of the same source fragment. Finally, we show that the algorithm can actually speed up the overall recompilation process, since checking for recompilation is always strictly less expensive than recompiling the same fragment.

[12] 
D. Ancona, G. Lagorio, and E. Zucca.
Jamdesigning a Java extension with mixins.
ACM Transactions on Programming Languages and Systems,
25(5):641712, September 2003.
[ bib 
.ps.gz 
http ]
In this paper we present Jam, an extension of the Java language supporting mixins, that is, parametric heir classes. A mixin declaration in Jam is similar to a Java heir class declaration, except that it does not extend a fixed parent class, but simply specifies 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 heirs, 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 by 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 somewhat 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.

[13] 
D. Ancona and E. Zucca.
A calculus of module systems.
Journ. of Functional Programming, 12(2):91132, 2002.
[ bib 
.ps.gz 
.html ]
We present CMS, a simple and powerful calculus of modules supporting mutual recursion and higher order features, which can be instantiated over an arbitrary core calculus satisfying standard assumptions. The calculus allows to express a large variety of existing mechanisms for combining software components, including parameterized modules like ML functors, extension with overriding of objectoriented programming, mixin modules and extralinguistic mechanisms like those provided by a linker. Hence CMS can be used as a paradigmatic calculus for modular languages, in the same spirit the lambda calculus is used for functional programming. As usual, we first present an untyped version of the calculus and then a type system; we prove the confluence, progress and subject reduction properties. Then, we show how it is possible to define a derived calculus of mixin modules directly in terms of CMS and to encode other primitive calculi (the lambda calculus and the AbadiCardelli's object calculus). Finally, we consider the problem of introducing a subtype relation for module types.

[14] 
D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini, and E. Zucca.
A type preserving translation of Fickle into Java.
Electronic Notes in Theoretical Computer Science. TOSCA 2001,
Theory of Concurrency, Higher Order Languages and Types, 62:6982, 2002.
[ bib 
.ps.gz 
http ]
We present a translation from Fickle (a Javalike language allowing objects that can change their class at runtime) into plain Java. The translation, which maps any Fickle class into a Java class, is driven by an invariant that relates the Fickle object to its Java counterpart. The translation, which is proven to preserve both the static and the dynamic semantics of the language, is an enhanced version of a previous proposal by the same authors.

[15] 
D. Ancona and E. Zucca.
A theory of mixin modules: Algebraic laws and reduction semantics.
Mathematical Structures in Computer Science, 12(6):701737,
2002.
[ bib 
.ps.gz ]
Mixins are modules which may contain deferred components, i.e. components not defined in the module itself; moreover, in contrast to parameterized modules (like ML functors), they can be mutually dependent and allow their definitions to be overridden. In a preceding paper we have defined syntax and denotational semantics of a kernel language of mixin modules. Here, we take instead an axiomatic approach, giving a set of algebraic laws expressing the expected properties of a small set of primitive operators on mixins. Interpreting axioms as rewriting rules, we get a reduction semantics for the language and prove the existence of normal forms. Moreover, we show that the model defined in the earlier paper satisfies the given axiomatization.

[16] 
D. Ancona and E. Zucca.
A theory of mixin modules: Basic and derived operators.
Mathematical Structures in Computer Science, 8(4):401446,
August 1998.
[ bib 
.ps.gz ]
Mixins are modules in which some components are deferred, i.e. their definition has to be provided by another module. Moreover, differently from parameterized modules (like ML functors), mixin modules can be mutually dependent and their composition supports redefinition of components (overriding). In this paper, we present a formal model of mixins and their basic composition operators. These operators can be viewed as 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. Our formal model is given in an "institution independent" way, i.e. is parameterized by the semantic framework modeling the underlying core language.

This file was generated by bibtex2html 1.98.