@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c 'keywords : "types"' /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@inproceedings{AnconaEtAl16,
author = {Ancona, D. and
Ferrando, A. and
Mascardi, V.},
title = {Comparing Trace Expressions and Linear Temporal Logic for Runtime
Verification},
booktitle = {Theory and Practice of Formal Methods - Essays Dedicated to Frank
de Boer on the Occasion of His 60th Birthday},
pages = {47--64},
year = {2016},
abstract = {{Trace expressions are a compact and expressive formalism, initially devised
for runtime verification of agent interactions in multiagent systems, which has been
successfully employed to model real protocols, and to generate monitors for mainstream multiagent system platforms,
and generalized to support runtime verification of different kinds of properties and systems.
In this paper we formally compare the expressive power of trace expressions with
the Linear Temporal Logic (LTL), a formalism widely adopted in runtime verification.
We show that any LTL formula can be translated into a trace expression
which is equivalent from the point of view of runtime verification.
Since trace expressions are able to express and verify sets of traces that
are not context-free, we can derive that in the context of runtime verification
trace expressions are more expressive than LTL.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaEtAlFdB16.pdf},
keywords = {agents, behavioral-types,runtime-verification}
}
@inproceedings{AnconaBFMT14,
author = {Ancona, Davide and
Briola, Daniela and
El Fallah{-}Seghrouchni, Amal and
Mascardi, Viviana and
Taillibert, Patrick},
title = {Exploiting Prolog for Projecting Agent Interaction Protocols},
booktitle = {Proceedings of the 29th Italian Conference on Computational Logic,
Torino, Italy, June 16-18, 2014.},
pages = {30--45},
year = {2014},
abstract = {{Constrained global types are a powerful means to represent agent interaction protocols. In our recent research we demonstrated that they can be used to represent complex protocols in a very compact way, and we exploited them to dynamically verify correct implementation of a protocol in a real MAS framework, Jason.
The main drawback of our previous approach is the full centralization of the monitoring activity which is delegated to a unique monitor agent.
This approach works well for MASs with few agents, but could become unsuitable in communication-intensive and highly-distributed MASs where hundreds of agents should be monitored.
In this paper we define an algorithm for projecting a constrained global type onto a set of agents Ags,
by restricting it to the interactions involving agents in Ags, so that the outcome of the algorithm is
another constrained global type that can be safely used for verifying the compliance of the sub-system Ags to the protocol specified by the original constrained global type.
The projection mechanism is implemented in SWI Prolog and is the first step towards distributing the monitoring activity, making it safer and more efficient: the compliance of a MAS to a protocol could be dynamically verified by suitably partitioning the agents of the MAS into small sets
of agents, and by assigning to each partition Ags a local monitor agent which checks all interactions involving Ags against the projected constrained global type.
We leave for further investigation the problem of finding suitable partitions of agents in a MAS, to guarantee that
verification through projected types and distributed agents is equivalent to verification
performed by a single centralized monitor with a unique global type.}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaBFMT14.pdf},
keywords = {agents, behavioral-types,runtime-verification}
}
@inproceedings{AnconaCorradi14,
booktitle = {{ECOOP 2014 - Object-Oriented Programming}},
keywords = {{objects,types,coinduction}},
note = {{To appear}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/CompleteCoinductiveSubtyping.pdf},
author = {Ancona, D. and Corradi, A.},
title = {{Sound and complete subtyping between coinductive types for object-oriented languages}},
year = {2014},
abstract = {Structural subtyping is an important notion for effective static type analysis;
it can be defined either axiomatically by a collection of subtyping rules, or by means of set inclusion between type interpretations, following
the semantic subtyping approach, which is more intuitive, and allows simpler proofs of the expected properties of the subtyping relation.
In object-oriented programming, recursive types typically correspond to inductively defined data structures, and subtyping is defined axiomatically;
however, in object-oriented languages objects can also be cyclic, but inductive types
cannot represent them as precisely as happens for coinductive types.
We study semantic subtyping between coinductive types with records and unions, which are particularly interesting for object-oriented programming,
show cases where it allows more precise type analysis, and develop a sound and complete effective algorithm for deciding it.
To our knowledge, this is the first proposal for a sound and complete algorithm for semantic subtyping between coinductive types.
}
}
@inproceedings{AnconaEtAl13a,
booktitle = {{ACM Symposium on Applied Computing (SAC 2013)}},
keywords = {{agents, behavioral-types,runtime-verification}},
note = {{Poster paper}},
author = {Ancona, D. and Barbieri, M. and Mascardi, V.},
title = {{Constrained Global Types for Dynamic Checking of Protocol Conformance in Multi-Agent Systems}},
pages = {1-3},
year = {2013},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ABM-SAC13.pdf},
abstract = {Global types are behavioral types for specifying and verifying multiparty
interactions between distributed components, inspired by the process algebra approach.
In this paper we extend the formalism of global types in multi-agent systems resulted from our previous work with a mechanism for easily expressing constrained shuffle of message sequences; accordingly, we extend the semantics to include the newly introduced feature, and show the expressive power of these ``constrained global types''.
}
}
@inproceedings{Ancona_FTfJP14,
booktitle = {{Formal techniques for Java-like programs (FTfJP14)}},
keywords = {{semantics, types, objects, coinduction}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/Ancona-FTfJP14.pdf},
author = {Ancona, D.},
title = {{How to Prove Type Soundness of Java-like Languages Without Forgoing Big-step Semantics}},
pages = {1:1--1:6},
year = {2014},
articleno = {1},
publisher = {ACM},
abstract = {Small-step operational semantics is the most commonly employed formalism for
proving type soundness of statically typed programming languages, because
of its ability to distinguish stuck from non-terminating computations,
as opposed to big-step operational semantics.
Despite this, big-step operational semantics is more abstract, and more
useful for specifying interpreters.
In previous work we have proposed a new proof technique to prove type soundness
of a Java-like language expressed in terms of its big-step operational semantics.
However the presented proof is rather involved, since it
requires showing that the set of proof trees defining the semantic judgment forms a complete metric space
when equipped with a specific distance function.
In this paper we propose a more direct and abstract approach that exploits a standard and general compactness property
of the metric space of values, that allows approximation of the coinductive big-step semantics in terms of the small-step one;
in this way type soundness can be proved by standard mathematical induction.
}
}
@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{AL-TCS12,
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},
series = {Lecture Notes in Computer Science},
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{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,runtime-verification},
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).},
pages = {1--20},
publisher = {Springer},
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, runtime-verification},
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
}
@inproceedings{MA-DALT11,
author = {Mascardi, V. and Ancona, D},
title = {1000 Years of Coo-{BDI}},
booktitle = {{D}eclarative {A}gent {L}anguages and {T}echnologies
{IX} - 9th {I}nternational {W}orkshop, {DALT} 2011,
Revised Selected and Invited Papers},
pages = {95-101},
abstract = {The idea of extending the BDI architecture with
cooperativity started shaping in 2003 when two
independent proposals to support cooperation in a BDI
setting were presented at DALT. One proposal, Coo-BDI,
extended the BDI architecture by allowing agents to
cooperate by exchanging and sharing plans in a quite
flexible way; the other extended the BDI operational
semantics for introducing speech-act based
communication, including primitives for plan exchange.
Besides allowing a natural and seamless integration
with speech-act based communication for BDI languages,
the intuitions behind Coo-BDI have proved to be
promising and attractive enough to give rise to new
investigations. In this retrospective review we discuss
papers that were influenced by Coo-BDI and we outline
other potential developments for future research.},
keywords = {agents, behavioral-types},
ftp = {http://www.disi.unige.it/person/MascardiV/Download/1000YearsCooBDI.pdf},
year = 2011
}
@inproceedings{MABR-IAT11,
author = {Mascardi, V. and Ancona, D. and Bordini, R. H. and
Ricci, A.},
title = {CooL-{A}gent{S}peak: {E}nhancing {A}gent{S}peak-{DL}
{A}gents with {P}lan {E}xchange and {O}ntology
{S}ervices},
booktitle = {Proceedings of the 2011 {IEEE}/{WIC}/{ACM}
{I}nternational {C}onference on {I}ntelligent {A}gent
{T}echnology, {IAT} 2011},
pages = {109-116},
abstract = {In this paper we present CooL-AgentSpeak, an extension
of AgentSpeak-DL with plan exchange and ontology
services. In CooL-AgentSpeak, the search for a plan is
no longer limited to the agent's local plan library but
is carried out in the other agents' libraries too,
according to a cooperation strategy, and it is not
based solely on unification and on the subsumption
relation between concepts, but also on ontology
matching. Belief querying and updating take advantage
of ontological reasoning and matching as well.},
keywords = {agents, behavioral-types},
ftp = {http://www.disi.unige.it/person/MascardiV/Download/IAT2011.pdf},
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
\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
}
@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{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{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
}
@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{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{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{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
}
@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
}
@inproceedings{ADDZ-FTfJP04,
author = {D.~Ancona and F.~Damiani and S.~Drossopoulou and
E.~Zucca},
title = {Even More Principal Typings for {J}ava-like Languages},
booktitle = {6th Intl. Workshop on Formal Techniques for Java Programs 2004},
abstract = {We propose an innovative type system for Java-like
languages which can infer the minimal set of
assumptions guaranteeing type correctness of a class c,
and generate (abstract) bytecode for c, by inspecting
the source code of c in isolation. We prove the above
properties of our type system by showing that it has
principal typings. As well known, principal typings
support compositional analysis, whereby a collection of
classes can be safely linked together without further
inspection of the classes' code, provided that each
class has been typechecked in isolation
(intra-checking), and that the mutual class assumptions
are satisfied (inter-checking). We also develop an
algorithm for inter-checking, and prove it correct. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FTfJP04.pdf},
keywords = {types, components},
month = jun,
year = 2004
}
@inproceedings{AM-GPCE04,
author = {Ancona, D. and Moggi, E.},
title = {A {F}resh {C}alculus for {N}ame {M}anagement},
booktitle = {Generative {P}rogramming and {C}omponent {E}ngineering
({GPCE} 2004)},
editor = {Karsai, G. and Visser, E.},
volume = {3286},
series = {Lecture Notes in Computer Science},
pages = {206--224},
publisher = {Springer Verlag},
abstract = {We define a basic calculus for name management, which
is obtained by an appropriate combination of three
ingredients: extensible records (in a simplified form),
names (as in FreshML), computational types (to allow
computational effects, including generation of fresh
names). The calculus supports the use of symbolic names
for programming in-the-large, e.g. it subsumes Ancona
and Zucca's calculus for module systems, and for
meta-programming (but not the intensional analysis of
object level terms supported by FreshML), e.g. it
subsumes (and improves) Nanevski and Pfenning's
calculus for meta-programming with names and necessity.
Moreover, it models some aspects of Java's class
loaders.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FCNM.pdf},
keywords = {meta-programming, types, components},
year = 2004
}
@inproceedings{FZA-SAC04,
author = {S.~Fagorzi and E.~Zucca and D.~Ancona},
title = {Modeling Multiple Class Loaders by a Calculus for
Dynamic Linking},
booktitle = {S{AC} 2004 - {P}roceedings of the 2004 {ACM}
{S}ymposium on {A}pplied {C}omputing},
editor = {Haddad, H. and Omicini, A. and Wainwright, R. L. and
Liebrock, L. M.},
pages = {1281--1288},
publisher = {ACM Press},
abstract = {A recent paper proposes a calculus for modeling
dynamic linking independently of the details of a
particular programming environment. Here we use a
particular instantiation of this calculus to encode a
toy language, called MCL, which provides an abstract
view of the mechanism of dynamic class loading with
multiple loaders as in Java. The aim is twofold. On one
hand, we show the effectiveness of the calculus in
modeling existing loading and linking policies. On the
other hand, we provide a simple formal model which
allows a better understanding of Java-like loading
mechanisms and also shows an intermediate solution
between the rigid approach based only on the classpath
and that which allows arbitrary user-defined loaders,
which can be intricate and error-prone.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/SAC04.ps.gz},
keywords = {types, components},
year = 2004
}
@inproceedings{AZ-POPL04,
author = {D.~Ancona and E.~Zucca},
title = {Principal Typings for {J}ava-like languages},
booktitle = {P{OPL} 2004 - {T}he 31st {ACM} {SIGPLAN}-{SIGACT}
{S}ymposium on {P}rinciples of {P}rogramming
{L}anguages},
pages = {306--317},
publisher = {ACM Press},
abstract = {The contribution of the paper is twofold. First, we
provide a general notion of type system supporting
separate compilation and inter-checking, and a formal
definition of soundess and completeness of
inter-checking w.r.t. global compilation. These
properties are important in practice since they allow
selective recompilation. In particular, we show that
they are guaranteed when the type system has principal
typings and provides sound and complete entailment
relation between type environments and types. The
second contribution is more specific, and is an
instantiation of the notion of type system previously
defined for Featherweight Java [IgarashiEtAl99] with
method overloading and field hiding. The aim is to show
that it is possible to define type systems for
Java-like languages, which, differently from those used
by standard compilers, have principal typings, hence
can be used as a basis for selective recompilation.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/POPL04.ps.gz},
keywords = {types, objects},
year = 2004
}
@inproceedings{AFZ-TCS04,
author = {D.~Ancona and S.~Fagorzi and E.~Zucca},
title = {A Calculus with Lazy Module Operators},
booktitle = {I{FIP} 18th {W}orld {C}omputer {C}ongress, {TC}1 3rd
{I}nt. {C}onf. on {T}heoretical {C}omputer {S}cience
({TCS}2004)},
editor = {Levy, J.-J. and Mayr, E. W. and Mitchell, J. C.},
pages = {423-436},
publisher = {Kluwer Academic Publishers},
abstract = {Modern programming environments such as those of Java
and C\# support dynamic loading of software fragments.
More in general, we can expect that in the future
systems will support more and more forms of
interleaving of reconfiguration steps and standard
execution steps, where the software fragments composing
a program are dynamically changed and/or combined on
demand and in different ways. However, existing kernel
calculi providing formal foundations for module systems
are based on a static view of module manipulation, in
the sense that open code fragments can be flexibly
combined together, but all module operators must be
performed once for all before starting execution of a
program, that is, evaluation of a module component. The
definition of clean and powerful module calculi
supporting lazy module operators, that is, operators
which can be performed after the selection of some
module component, is still an open problem. Here, we
provide an example in this direction (the first at our
knowledge), defining DCMS, an extension of the Calculus
of Module Systems where module operators can be
performed at execution time and, in particular, are
executed on demand, that is, only when needed by the
executing program. In other words, execution steps, if
possible, take the precedence over reconfiguration
steps. The type system of the calculus, which is proved
to be sound, relies on a dependency analysis which
ensures that execution will never try to access module
components which cannot become available by performing
reconfiguration steps.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/TCS04.pdf},
keywords = {types, components},
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
}
@inproceedings{AFMZ-ICALP03,
author = {D. Ancona and S. Fagorzi and E. Moggi and E. Zucca},
title = {Mixin Modules and Computational Effects},
booktitle = {I{CALP} 2003 - {A}utomata, {L}anguages and
{P}rogramming},
editor = {Goos, G. and Hartmanis, J. and van Leeuwen, J.},
volume = {2719},
series = {Lecture Notes in Computer Science},
pages = {224--238},
publisher = {Springer Verlag},
abstract = {We define a calculus for investigating the
interactions between mixin modules and computational
effects, by combining the purely functional mixin
calculus CMS with a monadic metalanguage supporting the
two separate notions of simplification (local rewrite
rules) and computation (global evaluation able to
modify the store). This distinction is important for
smoothly integrating the CMS rules (which are all
local) with the rules dealing with the imperative
features. In our calculus mixins can contain mutually
recursive computational components which are explicitly
computed by means of a new mixin operator whose
semantics is defined in terms of a Haskell-like
recursive monadic binding. Since we mainly focus on the
operational aspects, we adopt a simple type system like
that for Haskell, that does not detect dynamic errors
related to bad recursive declarations involving
effects. The calculus serves as a formal basis for
defining the semantics of imperative programming
languages supporting first class mixins while
preserving the CMS equational reasoning.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ICALP03.ps.gz},
keywords = {types, components},
year = 2003
}
@inproceedings{AL-FTfJP03,
author = {D.~Ancona and G.~Lagorio},
title = {Stronger Typings for Separate Compilation of
{J}ava-like Languages ({E}xtended {A}bstract)},
booktitle = {5th Intl. Workshop on Formal Techniques for Java Programs 2003},
abstract = {We define and implement a formal system supporting
separate compilation for a small but significant
Java-like language. This system is proved to be
stronger than the standard compilation of both Java and
C\#, in the sense that it better supports software
reuse by avoiding unnecessary recompilation steps after
code modification which are usually performed by using
the standard compilers. This is achieved by introducing
the notion of local type assumption allowing the user
to specify weaker requirements on the source fragments
which need to be compiled in isolation. Another
important property satisfied by our system is
compositionality, which corresponds to the intuition
that if a set of fragments can be separately compiled
and such fragments are compatible, then it is possible
to compile all the fragments together as a unique
program and obtain the same result.},
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},
url = {http://www.cs.ru.nl/ftfjp/2003.html},
year = 2003
}
@inproceedings{AFZ-ICTCS03,
author = {D. Ancona and S. Fagorzi and E. Zucca},
title = {A Calculus for Dynamic Linking},
booktitle = {I{CTCS} 2003 - {T}heoretical {C}omputer {S}cience},
editor = {C. Blundo and C. Laneve},
volume = {2841},
series = {Lecture Notes in Computer Science},
pages = {284--301},
publisher = {Springer Verlag},
abstract = {We define a calculus for modeling dynamic linking
independently of the details of a particular
programming environment. The calculus distinguishes at
the language level the notions of software
configuration and execution, by introducing separate
syntactic notions of linkset expression and command,
respectively. A reduction step can be either a
simplification of a linkset expression, or the
execution of a command w.r.t. a specific underlying
software configuration denoted by a linkset expression;
because of dynamic linking, these two kinds of
reductions are interleaved. The type system of the
calculus, which is proved to be sound, relies on an
accurate dependency analysis for ensuring type safety
without losing the advantages offered by dynamic
linking.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ICTCS03.ps.gz},
keywords = {types, components},
year = 2003
}
@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
}
@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
}
@inproceedings{ALZ-PPDP02,
author = {D. Ancona and G. Lagorio and E. Zucca},
title = {True Separate Compilation of {J}ava Classes},
booktitle = {A{CM} {SIGPLAN} {C}onference on {P}rinciples and
{P}ractice of {D}eclarative {P}rogramming ({PPDP}'02)},
pages = {189--200},
publisher = {ACM Press},
abstract = {We define a type system modeling true separate
compilation for a small but significant Java subset, in
the sense that a single class declaration can be
intra-checked (following the Cardelli's terminology)
and compiled providing a minimal set of type
requirements on missing classes. These requirements are
specified by a local type environment associated with
each single class, while in the existing formal
definitions of the Java type system classes are typed
in a global type environment containing all the type
information on a closed program. We also provide formal
rules for static inter-checking and relate our approach
with compilation of closed programs, by proving that we
get the same results. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/TrueSepCompLong.ps.gz},
keywords = {objects, types},
year = 2002
}
@inproceedings{ALZ-ECOOP02,
author = {D. Ancona and G. Lagorio and E. Zucca},
title = {A Formal Framework for {J}ava Separate Compilation},
booktitle = {E{COOP} 2002 - {O}bject-{O}riented {P}rogramming},
editor = {B. Magnusson},
volume = {2374},
series = {Lecture Notes in Computer Science},
pages = {609--635},
publisher = {Springer Verlag},
abstract = {We define a formal notion, called compilation schema,
allowing to specify different possibilities for
performing the overall process of Java compilation,
which includes type-checking of source fragments with
generation of corresponding binary code, type-checking
of binary fragments, extraction of type information
from fragments and definition of dependencies among
them. We consider three compilation schemata of
interest for Java, that is, minimal, SDK and safe,
which correspond to a minimal set of checks, the checks
performed by the SDK implementation, and all the checks
needed to prevent run-time linkage errors,
respectively. In order to demonstrate our approach, we
define a kernel model for Java separate compilation and
execution, consisting in a small Java subset, and a
simple corresponding binary language for which we
provide an operational semantics including run-time
verification. We define a safe compilation schema for
this language and formally prove type safety.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ECOOP02.ps.gz},
keywords = {objects, types},
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
}
@inproceedings{AZ-ECOOP01,
author = {D. Ancona and E. Zucca},
title = {True Modules for {J}ava-like Languages},
booktitle = {E{COOP} 2001 - {O}bject-{O}riented {P}rogramming},
editor = {J.L. Knudsen},
volume = {2072},
series = {Lecture Notes in Computer Science},
pages = {354--380},
publisher = {Springer Verlag},
abstract = {We present JavaMod, a true module system constructed
on top of a Java-like language. More in detail, this
means that basic modules are collections of Java
classes and specify in their interface the imported and
exported classes with their types; 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 designing such
a type system, one has to face non trivial problems,
notably the fact that a module M which extends an
imported class C can be correctly combined only with
modules exporting a class C which, besides providing
the expected services, causes no interferences with its
subclasses defined in M. What we obtain is a module
language which is extremely flexible and allows to
express (without any need of enriching the syntax of
the core level, that is, the Java language), for
instance, generic types as in Pizza and GJ, mixin
classes (that is, subclasses parametric in the direct
superclass) and mutually recursive class definitions
split in independent modules. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ECOOP01.ps.gz},
keywords = {objects, types, components},
year = 2001
}
@inproceedings{ALZ-FTfJP01,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {Java separate type checking is not safe},
booktitle = {3rd Intl. Workshop on Formal Techniques for Java Programs 2001},
abstract = {Java supports separate type-checking in the sense that
compilation can be invoked on a single source fragment,
and this may enforce type-checking of other either
source or binary fragments existing in the environment.
However, the Java specification does not define precise
rules on how this process should be performed,
therefore the outcome of compilation may strongly
depend on the particular compiler implementation.
Furthermore, rules adopted by standard Java compilers,
as SDK and Jikes, can produce binary fragments whose
execution throws linking related errors. We introduce a
simple framework which allows to formally express the
process of separate compilation and the related formal
notion of type safety. Moreover, we define, for a small
subset of Java, a type system for separate compilation
which we conjecture to be safe.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ECOOPWS01.ps.gz},
keywords = {objects, types},
url = {http://www.informatik.fernuni-hagen.de/pi5/tagungen/ecopp_2001/workshop_papers.htm},
year = 2001
}
@inproceedings{AADDGZ-ICTCS01,
author = {D. Ancona and C. Anderson and F. Damiani and S.
Drossopoulou and P. Giannini and E. Zucca},
title = {An Effective Translation of {F}ickle into {J}ava},
booktitle = {I{CTCS} 2001 - {T}heoretical {C}omputer {S}cience},
editor = {Restivo, A. and Ronchi Della Rocca, S. and Roversi, L.},
volume = {2202},
series = {Lecture Notes in Computer Science},
pages = {215-234},
publisher = {Springer Verlag},
abstract = {We present a translation from Fickle (a Java-like
language allowing dynamic object re-classification,
that is, objects that can change their class at
run-time) into plain Java. The translation is proved to
preserve static and dynamic semantics; moreover, it is
shown to be effective, in the sense that the
translation of a Fickle class does not depend on the
implementation of used classes, hence can be done in a
separate way, that is, without having their sources,
exactly as it happens for Java compilation. The aim is
to demonstrate that an extension of Java supporting
dynamic object re-classification could be fully
compatible with the existing Java environment. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/ICTCS01.ps.gz},
keywords = {objects, types},
year = 2001
}
@inproceedings{ALZ-OOPSLA01,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {A Core Calculus for {J}ava Exceptions},
booktitle = {A{CM} {C}onference on {O}bject-{O}riented
{P}rogramming, {S}ystems, {L}anguages, and
{A}pplications ({OOPSLA} 2001)},
series = {SIGPLAN Notices},
publisher = {ACM Press},
abstract = {In this paper we present a simple calculus (called
CJE) in order to fully investigate the exception
mechanism of Java, and in particular its interaction
with inheritance, which turns out to be non trivial.
Moreover, we show that the type system for the calculus
directly driven by the Java Language Specification
(called FULL) uses too many types, in the sense that
there are different types which provide exactly the
same information. Hence, we obtain from FULL a
simplified type system called MIN where equivalent
types have been identified. We show that this is useful
both for type-checking optimization and for clarifying
the static semantics of the language. The two type
systems are proved to satisfy the subject reduction
property.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/OOPSLA01.ps.gz},
keywords = {types, objects},
year = 2001
}
@inproceedings{ADZ-FOOL01,
author = {D.~Ancona and E.~Zucca and S.~Drossopoulou},
title = {Overloading and Inheritance},
booktitle = {The {E}ighth {I}nternational {W}orkshop on
{F}oundations of {O}bject-{O}riented {L}anguages
({FOOL}8)},
abstract = {Overloading allows several function definitions for
the same name, distinguished primarily through
different argument types; it is typically resolved at
compile-time. Inheritance allows subclasses to define
more special versions of the same function; it is
typically resolved at run-time. Modern object-oriented
languages incorporate both features, usually in a
type-safe manner. However, the combination of these
features sometimes turns out to have surprising, and
even counterintuitive, effects. We discuss why we
consider these effects inappropriate, and suggest
alternatives. We explore the design space by isolating
the main issues involved and analyzing their interplay
and suggest a formal framework describing static
overloading resolution and dynamic function selection,
abstracting from other language features. We believe
that our framework clarifies the thought process going
on at language design level. We introduce a notion of
soundness and completeness of an overloading resolution
policy w.r.t. the underlying dynamic semantics, and a
way of comparing the flexibility of different
resolution policies. We apply these concepts to some
non-trivial issues raised in concrete languages. We
also argue that the semantics of overloading and
inheritance is ``clean'' only if it can be understood
through a copy semantics, whereby programs are
transformed to equivalent programs without subclasses,
and the effect of inheritance is obtained through
copying. },
ftp = {http://www.cis.upenn.edu/~bcpierce/FOOL//FOOL8/Ancona.ps.gz},
keywords = {objects, types},
year = 2001
}
@inproceedings{ALZ-ECOOP00,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {{J}am: A Smooth Extension of {J}ava with Mixins},
booktitle = {E{COOP} 2000 - {O}bject-{O}riented {P}rogramming},
editor = {E. Bertino},
volume = {1850},
series = {Lecture Notes in Computer Science},
pages = {154--178},
publisher = {Springer Verlag},
abstract = {In this paper we present Jam, an extension of the Java
language supporting mixins, also called parametric heir
classes. A mixin declaration in Jam is similar to a
Java heir class declaration, apart that mixins do not
extend a fixed parent class, but simply specify 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 heir classes, 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 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 partly 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/ECOOP00.ps.gz},
keywords = {objects, types},
url = {http://www.disi.unige.it/person/LagorioG/jam/},
year = 2000
}
@inproceedings{ALZ-FTfJP00,
author = {D.~Ancona and G.~Lagorio and E.~Zucca},
title = {A Core Calculus for {J}ava Exceptions ({E}xtended
{A}bstract)},
booktitle = {2nd Intl. Workshop on Formal Techniques for Java Programs 2000},
abstract = {In this paper we present a simple calculus (called
CJE) corresponding to a small functional fragment of
Java supporting exceptions. We provide a reduction
semantics for the calculus together with two equivalent
type systems; the former corresponds to the standard
specication and its formalization, whereas the latter
can be considered an optimization of the former where
only the minimal type information about
classes/interfaces and methods are collected in order
to type-check a program. The two type systems are
proved to be equivalent and a subject reduction theorem
is given.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FTfJP00a.pdf},
keywords = {objects, types},
url = {http://www.informatik.fernuni-hagen.de/pi5/tagungen/ecoop_2000/workshop_papers.htm},
year = 2000
}
@inproceedings{AZD-FTfJP00,
author = {D.~Ancona and E.~Zucca and S.~Drossopoulou},
title = {Overloading and Inheritance in {J}ava ({E}xtended
{A}bstract)},
booktitle = {2nd Intl. Workshop on Formal Techniques for Java Programs 2000},
abstract = {The combination of overloading and inheritance in Java
introduces questions about function selection, and
makes some function calls ambiguous. We believe that
the approach taken by Java designers is
counterintuitive. We explore an alternative, and argue
that it is more intuitive and agrees with the Java
rules for the cases where Java considers the function
calls unambiguous, but gives meaning to more calls than
Java does.},
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/FTfJP00b.pdf},
keywords = {objects, types},
url = {http://www.informatik.fernuni-hagen.de/pi5/tagungen/ecoop_2000/workshop_papers.htm},
year = 2000
}
@inproceedings{AM-AGP00,
author = {Ancona, D. and Mascardi, V.},
title = {Mixin-based modules for logic programming},
booktitle = {A{PPIA}-{GULP}-{PRODE} 2000. 2000 {J}oint {C}onference
on {D}eclarative {P}rogramming},
abstract = {In this paper we show how it is possible to define a
rather rich language of mixin modules suitable for
combining together large logic programs without
changing the underlying logic. The type and reduction
rules for the language are presented in a somehow
informal way, whereas more emphasis is given to the
usefulness of the constructs from the programming point
of view and to the comparison with other proposals for
modular logic programming found in the literature. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/AGP00.ps.gz},
keywords = {components, types},
year = 2000
}
@inproceedings{AZ-PPDP99,
author = {D.~Ancona and E.~Zucca},
title = {A Primitive Calculus for Module Systems},
booktitle = {P{PDP}'99 - {I}nternational {C}onference of
{P}rinciples and {P}ractice of {D}eclarative
{P}rogramming},
editor = {G. Nadathur},
volume = {1702},
series = {Lecture Notes in Computer Science},
pages = {62--79},
publisher = {Springer Verlag},
abstract = {We present a simple and powerful calculus of modules
supporting mutual recursion and higher order features.
The calculus allows to encode 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. As usual,
we first present an untyped version of our calculus and
then a type system which is proved sound w.r.t. the
reduction semantics; moreover we give a translation of
other primitive calculi. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/PPDP99.ps.gz},
keywords = {components, types},
url = {http://www.disi.unige.it/person/AnconaD/Software/Java/CMS.html},
year = 1999
}
@inproceedings{Anc-WADT99,
author = {D. Ancona},
title = {An Algebraic Framework for Separate Type-Checking},
booktitle = {W{ADT}'98 - 13th {W}orkshop on {A}lgebraic
{D}evelopment {T}echniques - {S}elected {P}apers},
editor = {J. Fiadeiro},
volume = {1589},
series = {Lecture Notes in Computer Science},
pages = {1--15},
publisher = {Springer Verlag},
abstract = {We address the problem of defining an algebraic
framework for modularization supporting separate
type-checking. In order to do that we introduce the
notions of abstract type system and logic of
constraints and we present a canonical construction of
a model part, on top of a logic of constraints. This
canonical construction works under reasonable
assumptions on the underlying type system (e.g.,
soundness of the system). We show that the framework is
suitable for defining the static and dynamic semantics
of module languages, by giving a concrete example of
construction on top of the type system of a simple
typed module language. As a result, the subtyping
relation between module interfaces is captured in a
natural way by the notion of signature morphism. },
ftp = {ftp://ftp.disi.unige.it/pub/person/AnconaD/WADT98.ps.gz},
keywords = {semantics, types},
year = 1999
}
@inproceedings{BriolaMascardiAnconaIDC14,
author = {Briola, D. and
Mascardi, V. and
Ancona, D.},
title = {Distributed Runtime Verification of {JADE} Multiagent Systems},
booktitle = {Intelligent Distributed Computing {VIII} - Proceedings of the 8th
International Symposium on Intelligent Distributed Computing, {IDC}
2014, Madrid, Spain, September 3-5, 2014},
pages = {81--91},
year = {2014},
abstract = {{Verifying that agent interactions in a multiagent system (MAS) are compliant to a given global protocol is of paramount importance for most systems, and is mandatory for safety-critical applications. Runtime verification requires a proper formalism to express such a protocol, a possibly non intrusive mechanism for capturing agent interactions, and a method for verifying that captured interactions are compliant to the global protocol. Projecting the global protocol onto agents' subsets can improve efficiency and fault tolerance by allowing the distribution of the verification mechanism. Since many real MASs are based on JADE, a well known open source platform for MAS development, we implemented a monitor agent that achieves all the goals above using the "Attribute Global Types" (AGT) formalism for representing protocols. Using our JADE monitor we were able to verify FYPA, an extremely complex industrial MAS currently used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations, besides the Alternating Bit and the Iterated Contract Net protocols which are well known in the distributed systems and MAS communities. Depending on the monitored MAS, the performances of our monitor are either comparable or slightly worse than those of the JADE Sniffer because of the logging of the verification activities. Reducing the log files dimension, re-implementing the monitor in a way independent from the JADE Sniffer, and heavily exploiting projections are the three directions we are pursuing for improving the monitor's performances, still keeping all its features. }},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/IDC2014.pdf},
keywords = {runtime-verification, agents,behavioral-types}
}
@inproceedings{MascardiBriolaAnconaAIIA13,
author = {Mascardi, V. and
Briola, D. and
Ancona, D.},
title = {On the Expressiveness of Attribute Global Types: The Formalization
of a Real Multiagent System Protocol},
booktitle = {AI*IA 2013: Advances in Artificial Intelligence - XIIIth International
Conference of the Italian Association for Artificial Intelligence,
Turin, Italy, December 4-6, 2013. Proceedings},
pages = {300--311},
year = {2013},
abstract = {{Attribute global types are a formalism for specifying and dynamically verifying multi-party agents interaction protocols. They allow the multiagent system designer to easily express synchronization constraints among protocol branches and global constraints on sub-sequences of the allowed protocol traces. FYPA (Find Your Path, Agent!) is a multiagent system implemented in Jade currently being used by Ansaldo STS for allocating platforms and tracks to trains inside Italian stations. Since information on the station topology and on the current resource allocation is fully distributed, FYPA involves complex negotiation among agents to find a solution in quasi-real time. In this paper we describe the FYPA protocol using both AUML and attribute global types, showing that the second formalism is more concise than the first, besides being unambiguous and amenable for formal reasoning. Thanks to the Prolog implementation of the transition function defining the attribute global type semantic, we are able to generate a large number of protocol traces, and to manually inspect a subset of them to empirically validate that the protocol's formalization is correct. The integration of the Prolog verification mechanism into a Jade monitoring agent extending the Sniffer Agent is under way and will be used to verify the compliance of the actual conversation with the protocol. Keywords: multiagent systems, attribute global types, negotiation, dynamic verification of protocol compliance. }},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AIIA2013.pdf},
keywords = {runtime-verification, agents,behavioral-types}
}
@article{AnconaGianniniZucca16,
author = {Ancona, D. and
Giannini, P. and
Zucca, E.},
title = {Incremental Rebinding with Name Polymorphism},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {322},
pages = {19--34},
year = {2016},
url = {http://dx.doi.org/10.1016/j.entcs.2016.03.003},
doi = {10.1016/j.entcs.2016.03.003},
keywords = {types, components},
abstract = {{
We propose an extension with name variables of a calculus for incremental rebinding of code introduced in
previous work. Names, which can be either constants or variables, are used as interface of fragments of code
with free variables. Open code can be dynamically rebound by applying a rebinding, which is an association
from names to terms. Rebinding is incremental, since rebindings can contain free variables as well, and
can be manipulated by operators such as overriding and renaming. By using name variables, it is possible
to write terms which are parametric in their nominal interface and/or in the way it is adapted, greatly
enhancing expressivity. The type system is correspondingly extended by constrained name-polymorphic
types, where simple inequality constraints prevent conflicts among parametric name interfaces.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaGianniniZucca16.pdf}
}
@article{Betty16,
author = {Ancona, D. and
Bono, V. and
Bravetti, M. and
Campos, J. and
Castagna, G. and
Deni{\'{e}}lou, P.~M. and
Gay, S.~J. and
Gesbert, N. and
Giachino, E. and
Hu, R. and
Johnsen, E.~B. and
Martins, F. and
Mascardi, V. and
Montesi, F. and
Neykova, R. and
Ng, N. and
Padovani, L. and
Vasconcelos, V.T. and
Yoshida, N.},
title = {Behavioral Types in Programming Languages},
journal = {Foundations and Trends in Programming Languages},
volume = {3},
number = {2-3},
pages = {95--230},
year = {2016},
url = {http://dx.doi.org/10.1561/2500000031},
doi = {10.1561/2500000031},
keywords = {runtime-verification, agents,behavioral-types},
abstract = {{
A recent trend in programming language research is to use behavioral type theory to ensure various correctness properties of largescale, communication-intensive systems. Behavioral types encompass concepts such as interfaces, communication protocols, contracts, and choreography. The successful application of behavioral types requires a solid understanding of several practical aspects, from their representation in a concrete programming language, to their integration with other programming constructs such as methods and functions, to design and monitoring methodologies that take behaviors into account. This survey provides an overview of the state of the art of these aspects, which we summarize as the pragmatics of behavioral types.
}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/behavioralTypes.pdf}
}
@inproceedings{AnconaFerrandoMascardi17,
author = {Ancona, D. and
Ferrando, A. and
Mascardi, V.},
title = {Parametric Runtime Verification of Multiagent Systems},
booktitle = {Proceedings of the 16th Conference on Autonomous Agents and MultiAgent
Systems, {AAMAS} 2017, S{\~{a}}o Paulo, Brazil, May 8-12, 2017},
pages = {1457--1459},
year = {2017},
keywords = {runtime-verification, agents,behavioral-types},
abstract = {{
Parametricity is an important feature of a monitoring
system for making runtime verification (RV) more effective,
since, typically, correctness of traces depends on the specific
data values that are carried by the monitored events of the
trace, and that, in general, cannot be predicted statically.
Typically, the correctness of an interaction protocol may
depend on the values exchanged by agents; protocols may
also be parametric in the involved agents, and resources, and
this parametricity is naturally reflected on the data carried
by values.
In this work we propose parametric trace expressions, an
extension to trace expressions, expressly designed for
parametric RV of multiagent systems. Such an extension is
achieved by introducing variables in trace expressions that
are substituted with data values at runtime, when events are
matched during monitoring.
}},
http = {http://www.disi.unige.it/person/AnconaD/papers/AnconaFerrandoMascardiAAMAS17Parametric.pdf}
}
This file was generated by bibtex2html 1.98.