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