@comment{{This file has been generated by bib2bib 1.95}}
@comment{{Command line: bib2bib -c year>=2005 /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@techreport{AnconaExtendedSAC12,
author = {Ancona, D.},
title = {Regular corecursion in {P}rolog},
note = {Submitted for journal publication, extended version of
\url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#AnconaSAC12}{Ancona
at SAC12}},
institution = {DIBRIS - Universit\`a di Genova},
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 an interpreter where the search tree is pruned
to guarantee termination for certain kinds of predicate
definition; then we introduce \textbf{finally} clauses,
to provide a default value for all those cases where
unification with a coinductive hypothesis is not
correct. Finally, we propose a finer grain semantics
where the user can specify only a subset of the
arguments that have to be considered when coinductive
hypotheses are unified. The semantics defined by these
vanilla meta-interpreters are an interesting starting
point for a more mature design and implementation of
coinductive Prolog. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaExtendedSAC12.pdf},
keywords = {coinduction,corecursion},
year = 2012
}
@inproceedings{AMP-SAC12,
author = {Ancona, D. and Mascardi, V. and Pavarino, O.},
title = {Ontology-based documentation extraction for
semi-automatic migration of {J}ava code},
booktitle = {A{CM} {S}ymposium on {A}pplied {C}omputing ({SAC}
2012)},
editor = {Ossowski, S. and Lecca, P.},
pages = {1137--1143},
publisher = {ACM},
abstract = {Migrating libraries is not a trivial task, even under
the simplest assumption of a downward compatible
upgrade. We propose a novel approach to partially
relieve programmers from this task, based on the simple
observation that class, method and field names and
comments contained in a Java library should be a good
approximation of its semantics, and that code migration
requires knowing the semantic similarities between the
two libraries. Following this assumption, we borrow the
main concepts and notions from the Semantic Web, and
show how (1) an ontology can be automatically generated
from the relevant information extracted from the code
of the library; (2) semantic similarities between two
different libraries can be found by running a
particular ontology matching (a.k.a. ontology
alignment) algorithm on the two ontologies extracted
from the libraries. The main advantages of the approach
are that ontology extraction can be fully automated,
without adding ad-hoc code annotations, and that
results and tools produced by the Semantic Web research
community can be directly re-used for our purposes.
Experiments carried out even with simple and efficient
freely available matchers show that our approach is
promising, even though it would benefit from the use of
more advanced ontology matchers possibly integrated
with a component for checking type compatibility of the
computed alignments. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AMP-SAC12.pdf},
keywords = {agents, ontologies, refactoring},
year = 2012
}
@inproceedings{AnconaSAC12,
author = {Ancona, D.},
title = {Regular corecursion in {P}rolog},
booktitle = {A{CM} {S}ymposium on {A}pplied {C}omputing ({SAC}
2012)},
editor = {Ossowski, S. and Lecca, P.},
pages = {1897--1902},
abstract = {Co-recursion is the ability of defining a function
that produces some infinite data in terms of the
function and the data itself, and is typically
supported by languages with lazy evaluation. However,
in languages as Haskell strict operations fail to
terminate even on infinite regular data. Regular
co-recursion is naturally supported by co-inductive
Prolog, an extension where predicates can be
interpreted either inductively or co-inductively, that
has proved to be useful for formal verification, static
analysis and symbolic evaluation of programs. In this
paper we propose two main alternative vanilla
meta-interpreters to support regular co-recursion in
Prolog as an interesting programming style in its own
right, able to elegantly solve problems that would
require more complex code if conventional recursion
were used. In particular, the second meta-interpreters
avoids non termination in several cases, by restricting
the set of possible answers. The semantics defined by
these vanilla meta-interpreters are an interesting
starting point to study new semantics able to support
regular co-recursion for non logical languages. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaSAC12.pdf},
keywords = {coinduction,corecursion},
year = 2012
}
@inproceedings{AnconaECOOP12,
author = {Ancona, D.},
title = {Soundness of {O}bject-{O}riented {L}anguages with
{C}oinductive {B}ig-{S}tep {S}emantics},
booktitle = {E{COOP} 2012 - {O}bject-{O}riented {P}rogramming},
editor = {Noble, J.},
volume = {7313},
pages = {459--483},
publisher = {Springer},
abstract = {It is well known that big-step operational semantics
are not suitable for proving soundness of type systems,
because of their inability to distinguish stuck from
non-terminating computations. We show how this problem
can be solved by interpreting coinductively the rules
for the standard big-step operational semantics of a
Java-like language, thus making the claim of soundness
more intuitive: whenever a program is well-typed, its
coinductive operational semantics returns a value.
Indeed, coinduction allows non-terminating computations
to return values; this is proved by showing that the
set of proof trees defining the semantic judgment forms
a complete metric space when equipped with a proper
distance function. In this way, we are able to prove
soundness of a nominal type system w.r.t. the
coinductive semantics. Since the coinductive semantics
is sound w.r.t. the usual small-step operational
semantics, the standard claim of soundness can be
easily deduced. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaECOOP12.pdf},
keywords = {semantics, types, objects, coinduction},
year = 2012
}
@inproceedings{ALFoVeOOS11,
author = {Ancona, D. and Lagorio, G.},
title = {Static single information form for abstract
compilation},
booktitle = {Theoretical {C}omputer {S}cience ({IFIP} {TCS} 2012)},
editor = {Baeten, J. C.M. and Ball, T. and de Boer, F. S.},
volume = {7604},
pages = {10--27},
publisher = {Springer},
abstract = {In previous work we have shown that more precise type
analysis can be achieved by exploiting union types and
static single assignment (SSA) intermediate
representation (IR) of code. In this paper we exploit
static single information (SSI), an extension of SSA
proposed in literature and adopted by some compilers,
to allow assignments of more precise types to variables
in conditional branches. In particular, SSI can be
exploited rather easily and effectively to infer more
precise types in dynamic object-oriented languages,
where explicit runtime typechecking is frequently used.
We show how the use of SSI form can be smoothly
integrated with abstract compilation, our approach to
static type analysis. In particular, we define abstract
compilation based on union and nominal types for a
simple dynamic object-oriented language in SSI form
with a runtime typechecking operator, to show how
precise type inference can be.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AL-TCS12.pdf},
keywords = {objects,types,coinduction},
year = 2012
}
@inproceedings{AZ-CoLP12,
author = {Ancona, D. and Zucca, E.},
title = {Translating Corecursive {F}eatherweight {J}ava in
Coinductive Logic Programming},
booktitle = {{Co-LP} 2012 - A workshop on {C}oinductive {L}ogic
{P}rogramming},
abstract = {Corecursive FeatherWeight Java (coFJ) is a recently
proposed extension of the calculus FeatherWeight Java
(FJ), supporting cyclic objects and regular recursion,
and explicitly designed to promote a novel programming
paradigm inspired by coinductive Logic Programming
(coLP), based on coinductive, rather than inductive,
interpretation of recursive function definitions. We
present a slightly modified version of coFJ where the
application of a coinductive hypothesis can trigger the
evaluation of a specific expression at declaration,
rather than at use site. Following an approach inspired
by abstract compilation, we then show how coFJ can be
directly translated into coLP, when coinductive SLD is
extended with a similar feature for explicitly solving
a goal when a coinductive hypothesis is applied. Such a
translation is quite compact and, besides showing the
direct relation between coFJ and coinductive Prolog,
provides a first prototypical but simple and effective
implementation of coFJ.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-CoLP12.pdf},
keywords = {objects, coinduction, corecursion},
year = 2012
}
@inproceedings{ADM-DALT12,
author = {Ancona, D. and Drossopoulou, S. and Mascardi, V.},
title = {{Automatic Generation of Self-Monitoring MASs from
Multiparty Global Session Types in Jason}},
booktitle = {Declarative Agent Languages and Technologies (DALT
2012). Workshop Notes.},
pages = {1--17},
abstract = {Global session types are behavioral types designed for
specifying in a compact way multiparty interactions
between distributed components, and verifying their
correctness. We take advantage of the fact that global
session types can be naturally represented as cyclic
Prolog terms - which are directly supported by the
Jason implementation of AgentSpeak - to allow simple
automatic generation of self-monitoring MASs: given a
global session type specifying an interaction protocol,
and the implementation of a MAS where agents are
expected to be compliant with it, we define a procedure
for automatically deriving a self-monitoring MAS. Such
a generated MAS ensures that agents conform to the
protocol at run-time, by adding a monitor agent that
checks that the ongoing conversation is correct w.r.t.
the global session type. The feasibility of the
approach has been experimented in Jason for a
non-trivial example involving recursive global session
types with alternative choice and fork type
constructors. Although the main aim of this work is the
development of a unit testing framework for MASs, the
proposed approach can be also extended to implement a
framework supporting self-recovering MASs.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ADM-DALT12.pdf},
keywords = {agents, behavioral-types},
year = 2012
}
@inproceedings{ABM-ICTCS12,
author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
title = {Global {T}ypes for {D}ynamic {C}hecking of {P}rotocol
{C}onformance of {M}ulti-{A}gent {S}ystems ({E}xtended
{A}bstract)},
booktitle = {13th {I}talian {C}onference on {T}heoretical
{C}omputer {S}cience ({ICTCS} 2012)},
editor = {Massazza, P.},
pages = {39--43},
abstract = {In this paper we investigate the theoretical
foundations of global types for dynamic checking of
protocol compliance in multi-agents systems and we
extend the formalism by introducing a concatenation
operator that allows a significant enhancement of the
expressive power of global types. As examples, we show
how two non trivial protocols can be compactly
represented in the formalism: a ping-pong protocol, and
an alternating bit protocol, in the version proposed by
Deni\backslash{}'elou and Yoshida. Both protocols
cannot be specified easily (if at all) by other global
type frameworks, while in our approach they can be
expressed by two deterministic types (in a sense made
precise in the sequel) that can be effectively employed
for dynamic checking of the conformance to the
protocol.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-ICTCS12.pdf},
keywords = {agents, behavioral-types},
year = 2012
}
@inproceedings{AZ-FTfJP12,
author = {Ancona, D. and Zucca, E.},
title = {Corecursive {F}eatherweight {J}ava},
booktitle = {Formal techniques for {J}ava-like programs
({FT}f{JP}12)},
note = {To appear.},
abstract = {Despite cyclic data structures occur often in many
application domains, object-oriented programming
languages provide poor abstraction mechanisms for
dealing with cyclic objects. Such a deficiency is
reflected also in the research on theoretical
foundation of object-oriented languages; for instance,
Featherweigh Java (FJ), which is one of the most
widespread object-oriented calculi, does not allow
creation and manipulation of cyclic objects. We propose
an extension to Featherweight Java, called coFJ, where
it is possible to define cyclic objects, \{abstractly
corresponding to regular terms\}, and where an
abstraction mechanism, called regular corecursion, is
provided for supporting implementation of coinductive
operations on cyclic objects. We formally define the
operational semantics of coFJ, and provide a handful of
examples showing the expressive power of regular
corecursion; such a mechanism promotes a novel
programming style particularly well-suited for
implementing cyclic data structures, and for supporting
coinductive reasoning. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-FTfJP12.pdf},
keywords = {objects, coinduction, corecursion},
year = 2012
}
@inproceedings{AGZ-ITRS12,
author = {Ancona, D. and Giannini, P. and Zucca, E.},
title = {Reconciling positional and nominal binding},
booktitle = {Intersection {T}ypes and {R}elated {S}ystems ({ITRS}
2012)},
abstract = {We define an extension of the simply-typed lambda
calculus where two different binding mechanisms, by
position and by name, nicely coexist. In the former, as
in standard lambda calculus, the matching betweeen
parameter and argument is done on a positional basis,
hence alpha-equivalence holds, whereas in the latter it
is done on a nominal basis. The two mechanisms also
respectively correspond to static binding, where the
existence and type compatibility of the argument are
checked at compile-time, and dynamic binding, where
they are checked at runtime.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AGZ-ITRS12.pdf},
year = 2012
}
@inproceedings{ACLD10-FoVeOOS10,
author = {Ancona, D. and Corradi, A. and Lagorio, G. and
Damiani, F.},
title = {Abstract compilation of object-oriented languages into
coinductive {CLP}({X}): can type inference meet
verification?},
booktitle = {Formal {V}erification of {O}bject-{O}riented
{S}oftware {I}nternational {C}onference, {F}o{V}e{OOS}
2010, {P}aris, {F}rance, {J}une 28-30, 2010,
\textbf{{R}evised {S}elected {P}apers}},
editor = {Beckert, B. and March\'e, C.},
volume = {6528},
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
abstract = {This paper further investigates the potential and
practical applicability of abstract compilation in two
different directions. First, we formally define an
abstract compilation scheme for precise prediction of
uncaught exceptions for a simple Java-like language;
besides the usual user declared checked exceptions, the
analysis covers the runtime ClassCastException. Second,
we present a general implementation schema for abstract
compilation based on coinductive CLP with variance
annotation of user-defined predicates, and propose an
implementation based on a Prolog prototype
meta-interpreter, parametric in the solver for the
subtyping constraints.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ACLD10-FoVeOOS10.pdf},
keywords = {objects,types,coinduction},
year = 2011
}
@article{AL-RAIRO11,
author = {D. Ancona and G. Lagorio},
title = {Idealized coinductive type systems for imperative
object-oriented programs},
journal = {RAIRO - Theoretical Informatics and Applications},
volume = {45},
number = {1},
pages = {3-33},
abstract = {In recent work we have proposed a novel approach to
define idealized type systems for object-oriented
languages, based on abstract compilation of programs
into Horn formulas which are interpreted w.r.t. the
coinductive (that is, the greatest) Herbrand model. In
this paper we investigate how this approach can be
applied also in the presence of imperative features.
This is made possible by con- sidering a natural
translation of Static Single Assignment intermediate
form programs into Horn formulas, where phi functions
correspond to union types.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/RAIRO.pdf},
keywords = {objects,types,coinduction},
url = {http://www.rairo-ita.org},
year = 2011
}
@inproceedings{AnconaFTfJP11,
author = {Ancona, D.},
title = {Coinductive big-step operational semantics for type
soundness of {J}ava-like languages},
booktitle = {Formal {T}echniques for {J}ava-like {P}rograms
({FT}f{JP}11)},
pages = {5:1--5:6},
publisher = {ACM},
abstract = {We define a coinductive semantics for a simple
Java-like language by simply interpreting coinductively
the rules of a standard big-step operational semantics.
We prove that such a semantics is sound w.r.t. the
usual small-step operational semantics, and then prove
soundness of a conventional nominal type system w.r.t.
the coinductive semantics. From these two results,
soundness of the type system w.r.t. the small-step
semantics can be easily deduced. This new proposed
approach not only opens up new possibilities for
proving type soundness, but also provides useful
insights on the connection between coinductive big-step
operational semantics and type systems.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTfJP11.pdf},
isbn = {978-1-4503-0893-9},
keywords = {semantics, types, objects, coinduction},
year = 2011
}
@techreport{AL-10-11,
author = {Ancona, D. and Lagorio, G.},
title = {On sound and complete axiomatization of coinductive
subtyping for object-oriented languages},
institution = {DISI},
note = {Submitted for journal publication. Extended version of
\cite{AL-FTfJP10}},
abstract = {Coinductive abstract compilation is a novel technique,
which has been recently introduced for defining precise
type systems for object- oriented languages. In this
approach, type inference consists in translating the
program to be analyzed into a Horn formula f, and in
resolving a certain goal w.r.t. the coinductive (that
is, the greatest) Herbrand model of f. Type systems
defined in this way are idealized, since types and,
con- sequently, goal derivations, are not finitely
representable. Hence, sound implementable
approximations have to rely on the notions of regular
types and derivations, and of subtyping and subsumption
between types and atoms, respectively. In this paper we
address the problem of defining a sound and complete
axiomatization of a subtyping relation between
coinductive object and union types, defined as set
inclusion between type interpretations. Besides being
an important theoretical result, completeness is useful
for reasoning about possible implementations of the
subtyping relation, when restricted to regular types.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AL10-11.pdf},
keywords = {objects,types,coinduction},
month = nov,
year = 2010
}
@techreport{ACLD10-08-ext,
author = {Ancona, D. and Corradi, A. and Lagorio, G. and
Damiani, F.},
title = {Abstract compilation of object-oriented languages into
coinductive {CLP}({X}): can type inference meet
verification? (extended version)},
institution = {DISI},
note = {Extended version of \cite{ACLD10-FoVeOOS10}},
abstract = {This paper further investigates the potential and
practical applicability of abstract compilation in two
different directions. First, we formally define an
abstract compilation scheme for precise prediction of
uncaught exceptions for a simple Java-like language;
besides the usual user declared checked exceptions, the
analysis covers the runtime ClassCastException. Second,
we present a general implementation schema for abstract
compilation based on coinductive CLP with variance
annotation of user-defined predicates, and propose an
implementation based on a Prolog prototype
meta-interpreter, parametric in the solver for the
subtyping constraints. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ACLD10ext.pdf},
keywords = {objects,types,coinduction},
month = aug,
year = 2010
}
@inproceedings{AL-FTfJP10,
author = {D. Ancona and G. Lagorio},
title = {Complete coinductive subtyping for abstract
compilation of object-oriented languages},
booktitle = {F{TFJP} '10: {P}roceedings of the 12th {W}orkshop on
{F}ormal {T}echniques for {J}ava-{L}ike {P}rograms},
series = {ACM Digital Library},
pages = {1:1--1:7},
publisher = {ACM},
abstract = {Coinductive abstract compilation is a novel technique,
which has been recently introduced, for defining
precise type systems for object-oriented languages. In
this approach, type inference consists in translating
the program to be analyzed into a Horn formula f, and
in resolving a certain goal w.r.t. the coinductive
(that is, the greatest) Herbrand model of f. Type
systems defined in this way are idealized, since types
and, consequently, goal derivations, are not finitely
representable. Hence, sound implementable
approximations have to rely on the notions of regular
types and derivations, and of subtyping and subsumption
between types and atoms, respectively. In this paper we
address the problem of defining a complete subtyping
relation <= between types built on object and union
type constructors: we interpret types as sets of
values, and investigate on a definition of subtyping
such that t\_1 <= t\_2 is derivable whenever the
interpretation of t\_1 is contained in the
interpretation of t\_2. Besides being an important
theoretical result, completeness is useful for
reasoning about possible implementations of the
subtyping relation, when restricted to regular types. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTfJP10.pdf},
keywords = {objects,types,coinduction},
url = {http://portal.acm.org/citation.cfm?id=1924520},
year = 2010
}
@inproceedings{AL10-GandALF10,
author = {D. Ancona and G. Lagorio},
title = {Coinductive subtyping for abstract compilation of
object-oriented languages into {H}orn formulas},
booktitle = {Proceedings of {G}and{ALF} 2010},
editor = {{Montanari A.} and {Napoli M.} and {Parente M.}},
volume = {25},
series = {Electronic Proceedings in Theoretical Computer Science},
pages = {214--223},
abstract = {In recent work we have shown how it is possible to
define very precise type systems for object-oriented
languages by abstractly compiling a program into a Horn
formula f. Then type inference amounts to resolving a
certain goal w.r.t. the coinductive (that is, the
greatest) Herbrand model of f. Type systems defined in
this way are idealized, since in the most interesting
instantiations both the terms of the coinductive
Herbrand universe and goal derivations cannot be
finitely represented. However, sound and quite
expressive approximations can be implemented by
considering only regular terms and derivations. In
doing so, it is essential to introduce a proper
subtyping relation formalizing the notion of
approximation between types. In this paper we study a
subtyping relation on coinductive terms built on union
and object type constructors. We define an
interpretation of types as set of values induced by a
quite intuitive relation of membership of values to
types, and prove that the definition of subtyping is
sound w.r.t. subset inclusion between type
interpretations. The proof of soundness has allowed us
to simplify the notion of contractive derivation and to
discover that the previously given definition of
subtyping did not cover all possible representations of
the empty type. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/GandALF10.pdf},
keywords = {objects,types,coinduction},
year = 2010
}
@techreport{AnconaEtAl10,
author = {Ancona, D. and Corradi, A. and Lagorio, G. and
Damiani, F.},
title = {Abstract compilation of object-oriented languages into
coinductive {CLP}({X}): when type inference meets
verification},
institution = {Karlsruhe Institute of Technology},
note = {Formal {V}erification of {O}bject-{O}riented
{S}oftware. {P}apers presented at the {I}nternational
{C}onference, {J}une 28-30, 2010, {P}aris, {F}rance},
abstract = {We propose a novel general approach for defining
expressive type systems for object-oriented languages,
based on abstract compilation of programs into
coinductive constraint logic programs defined on a
specific constraint domain X called type domain. In
this way, type checking and type inference amount to
resolving a certain goal w.r.t. the coinductive (that
is, the greatest) Herbrand model of a logic program
(that is, a Horn formula) with constraints over a fixed
type domain X. In particular, we show an interesting
instantiation where the constraint predicates of X are
syntactic equality and subtyping over coinductive
object and union types. The corresponding type system
is so expressive to allow verification of simple
properties like data structure invariants. Finally, we
show a prototype implementation, written in Prolog, of
the inference engine for coinductive CLP(X), which is
parametric in the solver for the type domain X.},
booktitle = {Formal {V}erification of {O}bject-{O}riented
{S}oftware. {P}apers presented at the {I}nternational
{C}onference, {J}une 28-30, 2010, {P}aris, {F}rance},
editor = {Beckert, B. and March\'e, C.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FOVEOOS10-preproc.pdf},
keywords = {objects,types,coinduction},
publisher = {Karlsruhe},
series = {Karlsruhe Reports in Informatics (fr\"uher: Interner
Bericht. Fakult\"at f\"ur Informatik, Karlsruher
Institut f\"ur Technologie) ; 2010,13},
year = 2010
}
@inproceedings{AnconaMascardi-MALLOW-AWESOME09,
author = {Ancona, D. and Mascardi, V.},
title = {Exploiting {A}gents and {O}ntologies for {T}ype- and
{M}eaning-{S}afe {A}daptation of {J}ava {P}rograms},
booktitle = {Proceedings of the {MALLOW}-{AWESOME} 2009 workshop},
volume = {494},
publisher = {CEUR Workshop Proceedings},
abstract = {This paper discusses an application of intelligent
software agents and ontologies to solve the problem of
semi-automatic porting of Java programs. We have
designed a system for aiding users to adapt Java code
in a type- and meaning-safe way, when an application
has to migrate to new libraries which are not fully
compatible with the legacy ones. To achieve this, we
propose an approach based on an integration of the two
type-theoretic notions of subtyping and type
isomorphism with ontology matching. While the former
notions are needed to ensure flexible adaptation in the
presence of type-safety, the latter supports the user
to preserve the meaning of names that appear in the
program to be adapted. Intelligent agents control the
different components of the system and interact with
other agents in order to provide the final user with
the semi-automatic porting service he/she required.},
ftp = {http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-494/mallowawesomepaper6.pdf},
keywords = {agents,refactoring},
year = 2009
}
@inproceedings{CAR-ICOOLPS09,
author = {Cuni, A. and Ancona, D. and Rigo, A.},
title = {Faster than {C}\#: efficient implementation of dynamic
languages on {.NET}},
booktitle = {{ICOOOLPS} '09: Proceedings of the 4th workshop on the
{I}mplementation, {C}ompilation, {O}ptimization of
{O}bject-{O}riented {L}anguages and {P}rogramming
{S}ystems},
pages = {26--33},
address = {New York, NY, USA},
publisher = {ACM},
abstract = {The Common Language Infrastructure (CLI) is a virtual
machine expressly designed for implementing statically
typed languages such as C\#, therefore programs written
in dynamically typed languages are typically much
slower than C\# when executed on .NET. Recent
developments show that Just In Time (JIT) compilers can
exploit runtime type information to generate quite
efficient code. Unfortunately, writing a JIT compiler
is far from being simple. In this paper we report our
positive experience with automatic generation of JIT
compilers as supported by the PyPy infrastructure, by
focusing on JIT compilation for .NET. Following this
approach, we have in fact added a second layer of JIT
compilation, by allowing dynamic generation of more
efficient .NET bytecode, which in turn can be compiled
to machine code by the .NET JIT compiler. The main and
novel contribution of this paper is to show that this
two-layers JIT technique is effective, since programs
written in dynamic languages can run on .NET as fast as
(and in some cases even faster than) the equivalent C\#
programs. The practicality of the approach is
demonstrated by showing some promising experiments done
with benchmarks written in a simple dynamic language. },
doi = {http://doi.acm.org/10.1145/1565824.1565828},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ICOOOLPS09.pdf},
isbn = {978-1-60558-541-3},
keywords = {objects,dynamicLang},
location = {Genova, Italy},
year = 2009
}
@inproceedings{ALZ-TYPES08,
author = {Ancona, D. and Lagorio, G. and Zucca, E.},
title = {Type inference by coinductive logic programming},
booktitle = {Post-{P}roceedings of {TYPES} 2008},
editor = {Berardi S., Damiani F., de' Liguoro U.},
volume = {5497},
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
abstract = {We propose a novel approach to constraint-based type
inference based on coinductive logic programming. That
is, constraint generation corresponds to translation
into a conjunction of Horn clauses P, and constraint
satisfaction is defined in terms of the maximal
coinductive Herbrand model of P. We illustrate the
approach by formally defining this translation for a
small object-oriented language similar to Featherweight
Java, where type annotations in field and method
declarations can be omitted. In this way, we obtain a
very precise type inference and provide new insights
into the challenging problem of type inference for
object-oriented programs. Since the approach is
deliberately declarative, we define in fact a formal
specification for a general class of algorithms, which
can be a useful road maps to researchers. Moreover,
despite we consider here a particular language, the
methodology could be used in general for providing
abstract specifications of type inference for different
kinds of programming languages.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ALZ0908.pdf},
keywords = {objects,types,coinduction},
year = 2009
}
@inproceedings{AL-ECOOP09,
author = {Ancona, D. and Lagorio, G.},
title = {Coinductive type systems for object-oriented languages},
booktitle = {ECOOP 2009 - Object-Oriented Programming},
editor = {{S. Drossopoulou}},
volume = {5653},
series = {Lecture Notes in Computer Science},
pages = {2--26},
publisher = {Springer Verlag},
note = {\textbf{Best paper prize}},
abstract = {We propose a novel approach based on coinductive logic
to specify type systems of programming languages. The
approach consists in encoding programs in Horn formulas
which are interpreted w.r.t. their coinductive Herbrand
model. We illustrate the approach by first specifying a
standard type system for a small object-oriented
language similar to Featherweight Java. Then we define
an idealized type system for a variant of the language
where type annotations can be omitted. The type system
involves infinite terms and proof trees not
representable in a finite way, thus providing a
theoretical limit to type inference of object-oriented
programs, since only sound approximations of the system
can be implemented. Approximation is naturally captured
by the notions of subtyping and subsumption; indeed,
rather than increasing the expressive power of the
system, as it usually happens, here subtyping is needed
for approximating infinite non regular types and proof
trees with regular ones. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ECOOP09.pdf},
keywords = {objects,types,coinduction},
year = 2009
}
@techreport{ABCR1208,
author = {Ancona, D. and Bolz, C. and Cuni, A. and Rigo, A.},
title = {Automatic generation of {JIT} compilers for dynamic
languages in .{NET}},
institution = {Univ. of Dusseldorf and Univ. of Genova},
abstract = {Writing an optimizing static compiler for dynamic
languages is not an easy task, since quite complex
static analysis is required. On the other hand, recent
developments show that 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. The paper presents two main
and novel contributions: we show that partial
evaluation can be used in practice for generating a JIT
compiler, and we experiment with the potentiality
offered by the ability to add a further level of JIT
compilation on top of .NET. The practicality of the
approach is demonstrated by showing some promising
experiments done with benchmarks written in a simple
dynamic language.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABCR1208.pdf},
keywords = {objects,dynamicLang},
month = dec,
year = 2008
}
@techreport{AM1208,
author = {Ancona, D. and Mascardi, V.},
title = {Ontology matching for semi-automatic and type-safe
adaptation of {J}ava programs},
institution = {DISI - Univ. of Genova},
abstract = {This paper proposes a solution to the problem of
semi-automatic porting of Java programs. In particular,
our work aims at the design of tools able to aid users
to adapt Java code in a type-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 semantics of the program to be adapted.
},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AM1208.pdf},
keywords = {objects,types,refactoring},
month = dec,
year = 2008
}
@techreport{ALZ0708,
author = {Ancona, D. and Lagorio, G. and Zucca, E.},
title = {Type inference for {J}ava-like programs by coinductive
logic programming},
institution = {DISI - Univ. of Genova},
abstract = {Although coinductive logic programming (Co-LP) has
proved to have several applications, including
verification of infinitary properties, model checking
and bisimilarity proofs, type inference via Co-LP has
not been properly investigated yet. In this paper we
show a novel approach to solve the problem of type
inference in the context of Java-like languages, that
is, object-oriented languages based on nominal
subtyping. The proposed approach follows a generic
scheme: first, the program P to be analyzed is
translated into an approximating logic program P' and a
goal G; then, the solution of the type inference
problem corresponds to find an instantiation of the
goal G which belongs to the greatest model of P', that
is, the coinductive model of P'. Operationally, this
corresponds to find a co-SLD derivation of G in P',
according to the operational semantics of Co-LP
recently defined by Simon et al. [ICLP06,ICALP07]. A
complete formalization of an instantiation of this
scheme is considered for a simple object-oriented
language and a corresponding type soundness theorem is
stated. A prototype implementation based on a
meta-interpreter of co-SLD has been implemented.
Finally, we address scalability issues of the approach,
by sketching an instantiation able to deal with a much
more expressive object-oriented language.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ALZ0708.pdf},
keywords = {objects,types,coinduction},
month = jul,
year = 2008
}
@techreport{ALZ0408,
author = {Ancona, D. and Lagorio, G. and Zucca, E.},
title = {A flexible and type-safe framework of components for
{J}ava-like languages},
institution = {DISI - Univ. of Genova},
note = {Submitted for journal publication. Extended version of
this \url{Conferences.html#ALZ-JMLC06}{conference
paper}},
abstract = {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 that 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 that can be
instantiated on top of any Java-like language; to show
the effectiveness of the approach, an instantiation on
a small Java subset is provided, together with a
prototype implementation. 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. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTFCJL.pdf},
keywords = {objects,types,components},
month = apr,
year = 2008
}
@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
}
@inproceedings{ALZ-ICTCS07,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {Type inference for polymorphic methods in {J}ava-like
languages},
booktitle = {Theoretical {C}omputer {S}cience: {P}roceedings of the
10th {I}talian {C}onference on {ICTCS} '07},
editor = {Italiano, G. and Moggi, E. and Laura, L.},
publisher = {World Scientific},
note = {See also the
\url{ftp://ftp.disi.unige.it/pub/person/AnconaD/TIPMJLlong.pdf}{long
version} with proofs},
abstract = {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.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ALZ-ICTCS07.pdf},
keywords = {objects, types},
year = 2007
}
@inproceedings{AZ-ICTCS07,
author = {D.~Ancona and E.~Zucca},
title = {A formal framework for compositional compilation
(extended abstract)},
booktitle = {Theoretical {C}omputer {S}cience: {P}roceedings of the
10th {I}talian {C}onference on {ICTCS} '07},
editor = {Ancona, D. and Lagorio, G. and Zucca, E.},
publisher = {World Scientific},
note = {See also the
\url{ftp://ftp.disi.unige.it/pub/person/AnconaD/FFCClong.pdf}{long
version} with proofs and examples of framework
instantiation.},
abstract = {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.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/AZ-ICTCS07.pdf},
keywords = {types},
year = 2007
}
@inproceedings{AACM-DLS07,
author = {Ancona, D. and Ancona, M. and Cuni, A and Matsakis, N.},
title = {R{P}ython: a {S}tep {T}owards {R}econciling
{D}ynamically and {S}tatically {T}yped {OO} {L}anguages},
booktitle = {O{OPSLA} 2007 {P}roceedings and {C}ompanion, {DLS}'07:
{P}roceedings of the 2007 {S}ymposium on {D}ynamic
{L}anguages},
pages = {53--64},
publisher = {ACM},
abstract = {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.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/DLS08.pdf},
keywords = {objects,dynamicLang},
year = 2007
}
@inproceedings{ALZ-JMLC06,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {Flexible Type-Safe Linking of Components for
{J}ava-like Languages},
booktitle = {Joint {M}odular {L}anguages {C}onference ({JMLC} 2006)},
volume = {4228},
series = {Lecture Notes in Computer Science},
pages = {136--154},
publisher = {Springer Verlag},
note = {See also the \url{Reports.html#FTFCJL}{extended
version}},
abstract = {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. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/JMLC06.pdf},
keywords = {objects, types, components},
year = 2006
}
@inproceedings{ALZ-FTfJP05,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {Smart Modules for {J}ava-like Languages},
booktitle = {7th Intl. Workshop on Formal Techniques for Java-like Programs 2005},
abstract = {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.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/SMJL.pdf},
keywords = {types, objects, components},
month = jul,
year = 2005
}
@techreport{ADDZ05,
author = {D.~Ancona and F.~Damiani and S.~Drossopoulou and
E.~Zucca},
title = {Compositional {C}ompilation for {J}ava-like
{L}anguages through {P}olymorphic {B}ytecode},
institution = {Dipartimento di Informatica e Scienze dell'Informazione, Universit\`a di Genova},
abstract = {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).},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/PBCCJL.pdf},
keywords = {types, objects},
month = jan,
year = 2005
}
@inproceedings{MDA-WOA05,
author = {Mascardi, V. and Demergasso, D. and Ancona, D.},
title = {Languages for {P}rogramming {BDI}-style {A}gents: an
{O}verview},
booktitle = {W{OA} 2005 - {W}orkshop {F}rom {O}bjects to {A}gents},
editor = {Corradini, F. and De Paoli, F. and Merelli, E. and
Omicini, A.},
pages = {9--15},
abstract = {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. },
ftp = {http://www.disi.unige.it/person/MascardiV/Download/ancona-demergasso-mascardi-WOA05-final.pdf},
keywords = {agents},
year = 2005
}
@inproceedings{ADDZ-POPL05,
author = {D.~Ancona and F.~Damiani and S.~Drossopoulou and
E.~Zucca},
title = {Polymorphic Bytecode: Compositional Compilation for
{J}ava-like Languages},
booktitle = {P{OPL} 2005 - {T}he 32nd {ACM} {SIGPLAN}-{SIGACT}
{S}ymposium on {P}rinciples of {P}rogramming
{L}anguages},
pages = {26--37},
publisher = {ACM Press},
abstract = {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).},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/POPL05.pdf},
keywords = {types, objects},
year = 2005
}
@inproceedings{AFZ-TGC05,
author = {D.~Ancona and S.~Fagorzi and E.~Zucca},
title = {Mixin Modules for Dynamic Rebinding},
booktitle = {Trustworthy {G}lobal {C}omputing: {IST}/{FET}
{I}nternational {W}orkshop, {TGC} 2005, {E}dinburgh,
{UK}, {A}pril 7-9, 2005. {R}evised {S}elected {P}apers},
editor = {R. De Nicola and D. Sangiorgi},
volume = {3705},
series = {Lecture Notes in Computer Science},
pages = {279--298},
publisher = {Springer Verlag},
abstract = {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. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/TGC05.pdf},
keywords = {types, components},
year = 2005
}
@inproceedings{BMAB-EUMAS05,
author = {Bozzo, L. and Mascardi, V. and Ancona, D. and Busetta,
P.},
title = {C{OOWS}: {A}daptive {BDI} {A}gents meet
{S}ervice-{O}riented {C}omputing},
booktitle = {E{UMAS} 2005 - {P}roceedings of the {T}hird {E}uropean
{W}orkshop on {M}ulti-{A}gent {S}ystems, {B}russels,
{B}elgium, {D}ecember 7-8, 2005},
editor = {Gleizes, M. P. and Kaminka, G. A. and Now\'e, A. and
Ossowski, S. and Tuyls, K. and Verbeeck, K.},
pages = {473},
abstract = {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. },
ftp = {http://www.disi.unige.it/person/MascardiV/Download/coows4eumas.zip},
keywords = {agents},
year = 2005
}
@inproceedings{AM-FMCO05,
author = {Ancona, D. and Moggi, E.},
title = {Program {G}eneration and {C}omponents},
booktitle = {Formal {M}ethods for {C}omponents and {O}bjects:
{T}hird {I}nternational {S}ymposium, {FMCO} 2004},
editor = {de Boer, F. S. and Bonsangue, M. M. and Graf, S. and
de Roever, W.},
volume = {3657},
series = {Lecture Notes in Computer Science},
pages = {222--250},
publisher = {Springer Verlag},
abstract = {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).},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FMCO04.pdf},
keywords = {components, meta-programming, types},
year = 2005
}
@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
}
This file was generated by bibtex2html 1.95.