@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c $type="ARTICLE" /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@article{MascardiEtAl14,
keywords = {{agents}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/MABBR@WIAS14.pdf},
author = {Mascardi, V. and Ancona, D. and Barbieri, M. and Bordini, R. H. and Ricci, A.},
title = {{CooL-AgentSpeak: Endowing AgentSpeak-DL agents with plan exchange and ontology services}},
journal = {{Web Intelligence and Agent Systems}},
volume = {12},
number = {1},
pages = {83-107},
year = {2014},
abstract = { In this paper we present CooL-AgentSpeak, an extension of
AgentSpeak-DL with plan exchange and ontology services. In
CooL-AgentSpeak, the search for an ontologically relevant plan is no
longer limited to the agent's local plan library but is carried out
in the other agents' libraries too, according to a cooperation
strategy, and it is not based solely on unification and on the
subsumption relation between concepts, but also on ontology
matching. Belief querying and updating also take advantage of
ontological reasoning and matching.}
}
@article{AnconaDovier13,
keywords = {{coinduction}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaDovier14.pdf},
author = {Ancona, D. and Dovier, A.},
title = {{co-LP: Back to the Roots}},
journal = {{Theory and Practice of Logic Programming }},
volume = {13},
number = {4-5-Online-Supplement},
year = {2013},
abstract = {Recently, several papers dealing with co-inductive logic
programming have been proposed, dealing with pure Prolog and
constraint logic programming, with and without negation.
In this paper we revisit and use, as much as possible,
some fundamental results developed in the Eighties
to analyze the foundations,
and to clarify the possibilities but also
the intrinsic theoretical limits of this programming paradigm.
}
}
@article{AnconaCOMLAN13,
institution = {{DIBRIS - Universit{\`{a}} di Genova}},
keywords = {{coinduction,corecursion}},
note = {{Extended version of \url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#AnconaSAC12}{SAC 2012}}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/COMLAN13.pdf},
author = {Ancona, D.},
title = {{Regular corecursion in Prolog}},
journal = {{Computer Languages, Systems \& Structures}},
volume = {39},
number = {4},
pages = {142-162},
year = {2013},
abstract = {Corecursion is the ability of defining a function that
produces some infinite data in terms of the function
and the data itself, as supported by lazy evaluation.
However, in languages such as Haskell strict operations
fail to terminate even on infinite regular data, that
is, cyclic data. Regular corecursion is naturally
supported by coinductive Prolog, an extension where
predicates can be interpreted either inductively or
coinductively, that has proved to be useful for formal
verification, static analysis and symbolic evaluation
of programs. In this paper we use the meta-programming
facilities offered by Prolog to propose extensions to
coinductive Prolog aiming to make regular corecursion
more expressive and easier to program with. First, we
propose a new interpreter to solve the problem of
non-terminating failure as experienced with the
standard semantics of coinduction (as supported, for
instance, in SWI-Prolog). Another problem with the
standard semantics is that predicates expressed in
terms of existential quantification over a regular term
cannot directly defined by coinduction; to this aim, we
introduce finally clauses, to allow more flexibility in
coinductive definitions. Then we investigate the
possibility of annotating arguments of coinductive
predicates, to restrict coinductive definitions to a
subset of the arguments; this allows more efficient
definitions, and further enhance the expressive power
of coinductive Prolog. We investigate the effectiveness
of such features by showing different example programs
manipulating several kinds of cyclic values, ranging
from automata and context free grammars to graphs and
repeating decimals; the examples show how computations
on cyclic values can be expressed with concise and
relatively simple programs. The semantics defined by
these vanilla meta-interpreters are an interesting
starting point for a more mature design and
implementation of coinductive Prolog. }
}
@article{AL-RAIRO11,
author = {D. Ancona and G. Lagorio},
title = {Idealized coinductive type systems for imperative
object-oriented programs},
journal = {RAIRO - Theoretical Informatics and Applications},
volume = {45},
number = {1},
pages = {3-33},
abstract = {In recent work we have proposed a novel approach to
define idealized type systems for object-oriented
languages, based on abstract compilation of programs
into Horn formulas which are interpreted w.r.t. the
coinductive (that is, the greatest) Herbrand model. In
this paper we investigate how this approach can be
applied also in the presence of imperative features.
This is made possible by con- sidering a natural
translation of Static Single Assignment intermediate
form programs into Horn formulas, where phi functions
correspond to union types.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/RAIRO.pdf},
keywords = {objects,types,coinduction},
url = {http://www.rairo-ita.org},
year = 2011
}
@article{AFZ-ENTCS08,
author = {Ancona, D. and Fagorzi, S. and Zucca, E.},
title = {A parametric calculus for mobile open code},
journal = {Electronic Notes in Theoretical Computer Science},
volume = 192,
number = 3,
pages = {3 - 22},
note = {Proceedings of the Third International Workshop on
Developments in Computational Models (DCM 2007)},
abstract = {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 re-inspection 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
so-called 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 lambda-calculus 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 type-safe exchange of mobile code.},
doi = {DOI: 10.1016/j.entcs.2008.10.024},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ENTCS08.pdf},
keywords = {types, semantics},
url = {http://www.sciencedirect.com/science/article/B75H1-4TVSXYD-2/2/fa909596cba334aeb406667bdfd71e90},
year = 2008
}
@article{AADDGZ-TOPLAS07,
author = {D.~Ancona and C.~Anderson and F.~Damiani and
S.~Drossopoulou and P.~Giannini and E.~Zucca},
title = {A {P}rovenly {C}orrect {T}ranslation of {F}ickle into
{J}ava},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {29},
number = {2},
abstract = {We present a translation from Fickle, a small
object-oriented 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. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/TOPLAS07.pdf},
keywords = {objects, types},
month = apr,
year = 2007
}
@article{AFZ-ENTCS05,
author = {D.~Ancona and S.~Fagorzi and E.~Zucca},
title = {A Calculus for Dynamic Reconfiguration with Low
Priority Linking},
journal = {Electronic Notes in Theoretical Computer Science.
Proceedings of the Second Workshop on Object Oriented
Developments (WOOD 2004)},
volume = {138},
number = {2},
pages = {3-35},
abstract = {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. },
editor = {V. Bono and M. Bugliesi and S. Drossopoulou},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/WOOD04.pdf},
keywords = {components, types},
url = {http://www.sciencedirect.com/science?_ob=IssueURL&_tockey=%23TOC%2313109%232005%23998619997%23610759%23FLP%23&_auth=y&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=59a67baf997586dc2ab6a3f0a322dd50},
year = 2005
}
@article{AL-JOT04,
author = {D.~Ancona and G.~Lagorio},
title = {{S}tronger {T}ypings for {S}marter {R}ecompilation of
{J}ava-like {L}anguages},
journal = {Journal of Object Technology. Special issue. Workshop
on Formal Techniques for Java-like Programs (FTfJP)
ECOOP 2003},
volume = 3,
number = 6,
pages = {5-25},
abstract = {We define an algorithm for smarter recompilation of a
small but significant Java-like language; such an
algorithm is inspired by a type system previously
defined by Ancona and Zucca. In comparison with all
previous type systems for Java-like 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.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FTfJP03.ps.gz},
http = {http://www.disi.unige.it/person/AnconaD/Software/FJsc/},
keywords = {objects, types},
month = jun,
url = {http://www.jot.fm/issues/issue_2004_06/},
year = 2004
}
@article{ALZ-TOPLAS03,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {{Jam}--designing a {Java} extension with mixins},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {25},
number = {5},
pages = {641-712},
abstract = {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.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/TOPLAS03.ps.gz},
keywords = {objects, types},
month = sep,
url = {http://www.disi.unige.it/person/LagorioG/jam/},
year = 2003
}
@article{AZ-JFP02,
author = {D.~Ancona and E.~Zucca},
title = {A Calculus of Module Systems},
journal = {Journ. of Functional Programming},
volume = 12,
number = 2,
pages = {91-132},
abstract = {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 object-oriented programming, mixin
modules and extra-linguistic 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 Abadi-Cardelli's object
calculus). Finally, we consider the problem of
introducing a subtype relation for module types.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/JFP01.ps.gz},
keywords = {components, types},
url = {http://www.disi.unige.it/person/AnconaD/Software/Java/CMS.html},
year = 2002
}
@article{AADDGZ-ENTCS02,
author = {D. Ancona and C. Anderson and F. Damiani and S.
Drossopoulou and P. Giannini and E. Zucca},
title = {A Type Preserving Translation of {F}ickle into {J}ava},
journal = {Electronic Notes in Theoretical Computer Science.
TOSCA 2001, Theory of Concurrency, Higher Order
Languages and Types},
volume = 62,
pages = {69--82},
abstract = {We present a translation from Fickle (a Java-like
language allowing objects that can change their class
at run-time) 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. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ENTCS02.ps.gz},
keywords = {objects, types},
url = {http://www.sciencedirect.com/science?_ob=IssueURL&_tockey=%23TOC%2313109%232002%23999379999%23587065%23FLP%23&_auth=y&view=c&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=cf23278e62b455a161e5c672fa4bda20},
year = 2002
}
@article{AZ-MSCS02,
author = {D.~Ancona and E.~Zucca},
title = {A Theory of Mixin Modules: Algebraic Laws and
Reduction Semantics},
journal = {Mathematical Structures in Computer Science},
volume = 12,
number = {6},
pages = {701--737},
abstract = {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. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/MSCS01.ps.gz},
keywords = {components, semantics},
year = 2002
}
@article{AZ-MSCS98,
author = {D.~Ancona and E.~Zucca},
title = {A Theory of Mixin Modules: Basic and Derived Operators},
journal = {Mathematical Structures in Computer Science},
volume = 8,
number = 4,
pages = {401-446},
abstract = {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.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/MSCS98.ps.gz},
keywords = {components, semantics},
month = aug,
year = 1998
}
@article{AnconaDovierFI15,
author = {Ancona, D. and
Dovier, A.},
title = {A Theoretical Perspective of Coinductive Logic Programming},
journal = {Fundamenta Informaticae},
volume = {140},
number = {3-4},
pages = {221--246},
year = {2015},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaDovierFI15.pdf},
doi = {10.3233/FI-2015-1252},
keywords = {coinduction,logic programming},
abstract = {{
In this paper we study the semantics of Coinductive Logic Programming and
clarify its intrinsic computational limits, which prevent, in particular, the definition
of a complete, computable, operational semantics.
We propose a new operational semantics that allows a simple correctness result
and the definition of a simple meta-interpreter.
We compare, and prove the equivalence, with the operational semantics
defined and used in other papers on this topic.
}}
}
@article{AnconaGianniniZucca16,
author = {Ancona, D. and
Giannini, P. and
Zucca, E.},
title = {Incremental Rebinding with Name Polymorphism},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {322},
pages = {19--34},
year = {2016},
url = {http://dx.doi.org/10.1016/j.entcs.2016.03.003},
doi = {10.1016/j.entcs.2016.03.003},
keywords = {types, components},
abstract = {{
We propose an extension with name variables of a calculus for incremental rebinding of code introduced in
previous work. Names, which can be either constants or variables, are used as interface of fragments of code
with free variables. Open code can be dynamically rebound by applying a rebinding, which is an association
from names to terms. Rebinding is incremental, since rebindings can contain free variables as well, and
can be manipulated by operators such as overriding and renaming. By using name variables, it is possible
to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly
enhancing expressivity. The type system is correspondingly extended by constrained name-polymorphic
types, where simple inequality constraints prevent conflicts among parametric name interfaces.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaGianniniZucca16.pdf}
}
@article{Betty16,
author = {Ancona, D. and
Bono, V. and
Bravetti, M. and
Campos, J. and
Castagna, G. and
Deni{\'{e}}lou, P.~M. and
Gay, S.~J. and
Gesbert, N. and
Giachino, E. and
Hu, R. and
Johnsen, E.~B. and
Martins, F. and
Mascardi, V. and
Montesi, F. and
Neykova, R. and
Ng, N. and
Padovani, L. and
Vasconcelos, V.T. and
Yoshida, N.},
title = {Behavioral Types in Programming Languages},
journal = {Foundations and Trends in Programming Languages},
volume = {3},
number = {2-3},
pages = {95--230},
year = {2016},
url = {http://dx.doi.org/10.1561/2500000031},
doi = {10.1561/2500000031},
keywords = {runtime-verification, agents,behavioral-types},
abstract = {{
A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of largescale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/behavioralTypes.pdf}
}
This file was generated by bibtex2html 1.98.