@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c '$type="TECHREPORT" | $type="PHDTHESIS"' /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@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
\url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#AL-FTfJP10}{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 \url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#ACLD10-FoVeOOS10}{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
}
@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
}
@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
\url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#ALZ-JMLC06}{JMLC06}},
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
}
@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
}
@techreport{ALZ0802,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {Simplifying Types for a Calculus of {J}ava Exceptions},
institution = {Dipartimento di Informatica e Scienze dell'Informazione, Universit\`a di Genova},
note = {Submitted for journal publication},
abstract = {In this paper we present a simple calculus (called
CJE) in order to fully investigate the exception
mechanism of Java (in particular its interaction with
inheritance). We first define a type system for the
calculus, called FULL, directly driven by the Java
Language Specification and prove its soundness; then,
we show that this type system uses redundant types and
we formally capture this fact by defining equivalence
relations on types and by proving that the static
semantics of CJE programs is preserved under these
equivalences; furthermore, for each type we show that
there exists the smallest equivalent type. Finally, we
propose a simplification of the Java specification
concerning throws clause which minimally affects the
expressive power of the language.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/SimplExc.ps.gz},
keywords = {objects, types},
month = aug,
year = 2002
}
@techreport{AZ98,
author = {D.~Ancona and E.~Zucca},
title = {A Theory of Modules with State},
institution = {Dipartimento di Informatica e Scienze dell'Informazione, Universit\`a di Genova},
number = {DISI-TR-98-10},
abstract = {We propose a new way of handling imperative features
in the algebraic approach to composition of software
modules, meant in its abstract categorical formulation.
The basic idea is to consider, instead of a global
state, orthogonal to the modular structure, the local
state of a module as the collection of those components
which have no associated definition but an extension
which may vary dynamically. Following this intuition,
composition of modules via classical operators like
merge, renaming and hiding involves composition of the
corresponding states, allowing one to give a truly
compositional semantics of module languages. Thanks to
the abstract categorical formulation, we are able to
define a canonical construction of a framework for
modules with state starting from a framework with no
imperative features. This provides the theoretical
basis for designing languages of modules with state in
a way independent of the underlying core language.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/DISI-TR-98-10.ps.gz},
keywords = {components, semantics},
year = 1998
}
@phdthesis{Anc98,
author = {D.~Ancona},
title = {Modular Formal Frameworks for Module Systems},
school = {Dipartimento di Informatica, Universit\`a di Pisa},
abstract = {In this thesis we present two formal frameworks for
modeling modular languages. Following a modular
approach, we separate the module and the core level of
a modular language. On the linguistic side, this
corresponds to define a kernel module language
parametric in the underlying core language. On the
semantic side, this corresponds to build a model part
(in the sense of institutions), on top of a standard
module framework. The standard module framework is a
model part, too, satisfying some additional properties
and intended as the formal counterpart of the core
language. The first formal framework we propose deals
with the notion of state, an essential component of
modules in imperative languages. The second one is
concerned with a notion of module, called mixin, which
includes those of generic module and abstract class. In
both cases, we present two canonical constructions
yielding a formal framework where models denote modules
with state and mixins, respectively, and we define a
set of primitive operations over them. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/PhDthesis.ps.gz},
keywords = {semantics, components, objects},
number = {TD-1/98},
year = 1998
}
This file was generated by bibtex2html 1.98.