@comment{{This file has been generated by bib2bib 1.95}}
@comment{{Command line: bib2bib -c $type="ARTICLE" /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@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
}
This file was generated by bibtex2html 1.95.