@comment{{This file has been generated by bib2bib 1.95}}
@comment{{Command line: bib2bib -c 'keywords : "coinduction"' /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@techreport{AnconaExtendedSAC12,
author = {Ancona, D.},
title = {Regular corecursion in {P}rolog},
note = {Submitted for journal publication, extended version of
\url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#AnconaSAC12}{Ancona
at SAC12}},
institution = {DIBRIS - Universit\`a di Genova},
abstract = {Corecursion is the ability of defining a function that
produces some infinite data in terms of the function
and the data itself, as supported by lazy evaluation.
However, in languages such as Haskell strict operations
fail to terminate even on infinite regular data, that
is, cyclic data. Regular corecursion is naturally
supported by coinductive Prolog, an extension where
predicates can be interpreted either inductively or
coinductively, that has proved to be useful for formal
verification, static analysis and symbolic evaluation
of programs. In this paper we use the meta-programming
facilities offered by Prolog to propose extensions to
coinductive Prolog aiming to make regular corecursion
more expressive and easier to program with. First, we
propose an interpreter where the search tree is pruned
to guarantee termination for certain kinds of predicate
definition; then we introduce \textbf{finally} clauses,
to provide a default value for all those cases where
unification with a coinductive hypothesis is not
correct. Finally, we propose a finer grain semantics
where the user can specify only a subset of the
arguments that have to be considered when coinductive
hypotheses are unified. The semantics defined by these
vanilla meta-interpreters are an interesting starting
point for a more mature design and implementation of
coinductive Prolog. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaExtendedSAC12.pdf},
keywords = {coinduction,corecursion},
year = 2012
}
@inproceedings{AnconaSAC12,
author = {Ancona, D.},
title = {Regular corecursion in {P}rolog},
booktitle = {A{CM} {S}ymposium on {A}pplied {C}omputing ({SAC}
2012)},
editor = {Ossowski, S. and Lecca, P.},
pages = {1897--1902},
abstract = {Co-recursion is the ability of defining a function
that produces some infinite data in terms of the
function and the data itself, and is typically
supported by languages with lazy evaluation. However,
in languages as Haskell strict operations fail to
terminate even on infinite regular data. Regular
co-recursion is naturally supported by co-inductive
Prolog, an extension where predicates can be
interpreted either inductively or co-inductively, that
has proved to be useful for formal verification, static
analysis and symbolic evaluation of programs. In this
paper we propose two main alternative vanilla
meta-interpreters to support regular co-recursion in
Prolog as an interesting programming style in its own
right, able to elegantly solve problems that would
require more complex code if conventional recursion
were used. In particular, the second meta-interpreters
avoids non termination in several cases, by restricting
the set of possible answers. The semantics defined by
these vanilla meta-interpreters are an interesting
starting point to study new semantics able to support
regular co-recursion for non logical languages. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaSAC12.pdf},
keywords = {coinduction,corecursion},
year = 2012
}
@inproceedings{AnconaECOOP12,
author = {Ancona, D.},
title = {Soundness of {O}bject-{O}riented {L}anguages with
{C}oinductive {B}ig-{S}tep {S}emantics},
booktitle = {E{COOP} 2012 - {O}bject-{O}riented {P}rogramming},
editor = {Noble, J.},
volume = {7313},
pages = {459--483},
publisher = {Springer},
abstract = {It is well known that big-step operational semantics
are not suitable for proving soundness of type systems,
because of their inability to distinguish stuck from
non-terminating computations. We show how this problem
can be solved by interpreting coinductively the rules
for the standard big-step operational semantics of a
Java-like language, thus making the claim of soundness
more intuitive: whenever a program is well-typed, its
coinductive operational semantics returns a value.
Indeed, coinduction allows non-terminating computations
to return values; this is proved by showing that the
set of proof trees defining the semantic judgment forms
a complete metric space when equipped with a proper
distance function. In this way, we are able to prove
soundness of a nominal type system w.r.t. the
coinductive semantics. Since the coinductive semantics
is sound w.r.t. the usual small-step operational
semantics, the standard claim of soundness can be
easily deduced. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AnconaECOOP12.pdf},
keywords = {semantics, types, objects, coinduction},
year = 2012
}
@inproceedings{ALFoVeOOS11,
author = {Ancona, D. and Lagorio, G.},
title = {Static single information form for abstract
compilation},
booktitle = {Theoretical {C}omputer {S}cience ({IFIP} {TCS} 2012)},
editor = {Baeten, J. C.M. and Ball, T. and de Boer, F. S.},
volume = {7604},
pages = {10--27},
publisher = {Springer},
abstract = {In previous work we have shown that more precise type
analysis can be achieved by exploiting union types and
static single assignment (SSA) intermediate
representation (IR) of code. In this paper we exploit
static single information (SSI), an extension of SSA
proposed in literature and adopted by some compilers,
to allow assignments of more precise types to variables
in conditional branches. In particular, SSI can be
exploited rather easily and effectively to infer more
precise types in dynamic object-oriented languages,
where explicit runtime typechecking is frequently used.
We show how the use of SSI form can be smoothly
integrated with abstract compilation, our approach to
static type analysis. In particular, we define abstract
compilation based on union and nominal types for a
simple dynamic object-oriented language in SSI form
with a runtime typechecking operator, to show how
precise type inference can be.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AL-TCS12.pdf},
keywords = {objects,types,coinduction},
year = 2012
}
@inproceedings{AZ-CoLP12,
author = {Ancona, D. and Zucca, E.},
title = {Translating Corecursive {F}eatherweight {J}ava in
Coinductive Logic Programming},
booktitle = {{Co-LP} 2012 - A workshop on {C}oinductive {L}ogic
{P}rogramming},
abstract = {Corecursive FeatherWeight Java (coFJ) is a recently
proposed extension of the calculus FeatherWeight Java
(FJ), supporting cyclic objects and regular recursion,
and explicitly designed to promote a novel programming
paradigm inspired by coinductive Logic Programming
(coLP), based on coinductive, rather than inductive,
interpretation of recursive function definitions. We
present a slightly modified version of coFJ where the
application of a coinductive hypothesis can trigger the
evaluation of a specific expression at declaration,
rather than at use site. Following an approach inspired
by abstract compilation, we then show how coFJ can be
directly translated into coLP, when coinductive SLD is
extended with a similar feature for explicitly solving
a goal when a coinductive hypothesis is applied. Such a
translation is quite compact and, besides showing the
direct relation between coFJ and coinductive Prolog,
provides a first prototypical but simple and effective
implementation of coFJ.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-CoLP12.pdf},
keywords = {objects, coinduction, corecursion},
year = 2012
}
@inproceedings{AZ-FTfJP12,
author = {Ancona, D. and Zucca, E.},
title = {Corecursive {F}eatherweight {J}ava},
booktitle = {Formal techniques for {J}ava-like programs
({FT}f{JP}12)},
note = {To appear.},
abstract = {Despite cyclic data structures occur often in many
application domains, object-oriented programming
languages provide poor abstraction mechanisms for
dealing with cyclic objects. Such a deficiency is
reflected also in the research on theoretical
foundation of object-oriented languages; for instance,
Featherweigh Java (FJ), which is one of the most
widespread object-oriented calculi, does not allow
creation and manipulation of cyclic objects. We propose
an extension to Featherweight Java, called coFJ, where
it is possible to define cyclic objects, \{abstractly
corresponding to regular terms\}, and where an
abstraction mechanism, called regular corecursion, is
provided for supporting implementation of coinductive
operations on cyclic objects. We formally define the
operational semantics of coFJ, and provide a handful of
examples showing the expressive power of regular
corecursion; such a mechanism promotes a novel
programming style particularly well-suited for
implementing cyclic data structures, and for supporting
coinductive reasoning. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-FTfJP12.pdf},
keywords = {objects, coinduction, corecursion},
year = 2012
}
@inproceedings{ACLD10-FoVeOOS10,
author = {Ancona, D. and Corradi, A. and Lagorio, G. and
Damiani, F.},
title = {Abstract compilation of object-oriented languages into
coinductive {CLP}({X}): can type inference meet
verification?},
booktitle = {Formal {V}erification of {O}bject-{O}riented
{S}oftware {I}nternational {C}onference, {F}o{V}e{OOS}
2010, {P}aris, {F}rance, {J}une 28-30, 2010,
\textbf{{R}evised {S}elected {P}apers}},
editor = {Beckert, B. and March\'e, C.},
volume = {6528},
series = {Lecture Notes in Computer Science},
publisher = {Springer Verlag},
abstract = {This paper further investigates the potential and
practical applicability of abstract compilation in two
different directions. First, we formally define an
abstract compilation scheme for precise prediction of
uncaught exceptions for a simple Java-like language;
besides the usual user declared checked exceptions, the
analysis covers the runtime ClassCastException. Second,
we present a general implementation schema for abstract
compilation based on coinductive CLP with variance
annotation of user-defined predicates, and propose an
implementation based on a Prolog prototype
meta-interpreter, parametric in the solver for the
subtyping constraints.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ACLD10-FoVeOOS10.pdf},
keywords = {objects,types,coinduction},
year = 2011
}
@article{AL-RAIRO11,
author = {D. Ancona and G. Lagorio},
title = {Idealized coinductive type systems for imperative
object-oriented programs},
journal = {RAIRO - Theoretical Informatics and Applications},
volume = {45},
number = {1},
pages = {3-33},
abstract = {In recent work we have proposed a novel approach to
define idealized type systems for object-oriented
languages, based on abstract compilation of programs
into Horn formulas which are interpreted w.r.t. the
coinductive (that is, the greatest) Herbrand model. In
this paper we investigate how this approach can be
applied also in the presence of imperative features.
This is made possible by con- sidering a natural
translation of Static Single Assignment intermediate
form programs into Horn formulas, where phi functions
correspond to union types.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/RAIRO.pdf},
keywords = {objects,types,coinduction},
url = {http://www.rairo-ita.org},
year = 2011
}
@inproceedings{AnconaFTfJP11,
author = {Ancona, D.},
title = {Coinductive big-step operational semantics for type
soundness of {J}ava-like languages},
booktitle = {Formal {T}echniques for {J}ava-like {P}rograms
({FT}f{JP}11)},
pages = {5:1--5:6},
publisher = {ACM},
abstract = {We define a coinductive semantics for a simple
Java-like language by simply interpreting coinductively
the rules of a standard big-step operational semantics.
We prove that such a semantics is sound w.r.t. the
usual small-step operational semantics, and then prove
soundness of a conventional nominal type system w.r.t.
the coinductive semantics. From these two results,
soundness of the type system w.r.t. the small-step
semantics can be easily deduced. This new proposed
approach not only opens up new possibilities for
proving type soundness, but also provides useful
insights on the connection between coinductive big-step
operational semantics and type systems.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTfJP11.pdf},
isbn = {978-1-4503-0893-9},
keywords = {semantics, types, objects, coinduction},
year = 2011
}
@techreport{AL-10-11,
author = {Ancona, D. and Lagorio, G.},
title = {On sound and complete axiomatization of coinductive
subtyping for object-oriented languages},
institution = {DISI},
note = {Submitted for journal publication. Extended version of
\cite{AL-FTfJP10}},
abstract = {Coinductive abstract compilation is a novel technique,
which has been recently introduced for defining precise
type systems for object- oriented languages. In this
approach, type inference consists in translating the
program to be analyzed into a Horn formula f, and in
resolving a certain goal w.r.t. the coinductive (that
is, the greatest) Herbrand model of f. Type systems
defined in this way are idealized, since types and,
con- sequently, goal derivations, are not finitely
representable. Hence, sound implementable
approximations have to rely on the notions of regular
types and derivations, and of subtyping and subsumption
between types and atoms, respectively. In this paper we
address the problem of defining a sound and complete
axiomatization of a subtyping relation between
coinductive object and union types, defined as set
inclusion between type interpretations. Besides being
an important theoretical result, completeness is useful
for reasoning about possible implementations of the
subtyping relation, when restricted to regular types.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AL10-11.pdf},
keywords = {objects,types,coinduction},
month = nov,
year = 2010
}
@techreport{ACLD10-08-ext,
author = {Ancona, D. and Corradi, A. and Lagorio, G. and
Damiani, F.},
title = {Abstract compilation of object-oriented languages into
coinductive {CLP}({X}): can type inference meet
verification? (extended version)},
institution = {DISI},
note = {Extended version of \cite{ACLD10-FoVeOOS10}},
abstract = {This paper further investigates the potential and
practical applicability of abstract compilation in two
different directions. First, we formally define an
abstract compilation scheme for precise prediction of
uncaught exceptions for a simple Java-like language;
besides the usual user declared checked exceptions, the
analysis covers the runtime ClassCastException. Second,
we present a general implementation schema for abstract
compilation based on coinductive CLP with variance
annotation of user-defined predicates, and propose an
implementation based on a Prolog prototype
meta-interpreter, parametric in the solver for the
subtyping constraints. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/ACLD10ext.pdf},
keywords = {objects,types,coinduction},
month = aug,
year = 2010
}
@inproceedings{AL-FTfJP10,
author = {D. Ancona and G. Lagorio},
title = {Complete coinductive subtyping for abstract
compilation of object-oriented languages},
booktitle = {F{TFJP} '10: {P}roceedings of the 12th {W}orkshop on
{F}ormal {T}echniques for {J}ava-{L}ike {P}rograms},
series = {ACM Digital Library},
pages = {1:1--1:7},
publisher = {ACM},
abstract = {Coinductive abstract compilation is a novel technique,
which has been recently introduced, for defining
precise type systems for object-oriented languages. In
this approach, type inference consists in translating
the program to be analyzed into a Horn formula f, and
in resolving a certain goal w.r.t. the coinductive
(that is, the greatest) Herbrand model of f. Type
systems defined in this way are idealized, since types
and, consequently, goal derivations, are not finitely
representable. Hence, sound implementable
approximations have to rely on the notions of regular
types and derivations, and of subtyping and subsumption
between types and atoms, respectively. In this paper we
address the problem of defining a complete subtyping
relation <= between types built on object and union
type constructors: we interpret types as sets of
values, and investigate on a definition of subtyping
such that t\_1 <= t\_2 is derivable whenever the
interpretation of t\_1 is contained in the
interpretation of t\_2. Besides being an important
theoretical result, completeness is useful for
reasoning about possible implementations of the
subtyping relation, when restricted to regular types. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FTfJP10.pdf},
keywords = {objects,types,coinduction},
url = {http://portal.acm.org/citation.cfm?id=1924520},
year = 2010
}
@inproceedings{AL10-GandALF10,
author = {D. Ancona and G. Lagorio},
title = {Coinductive subtyping for abstract compilation of
object-oriented languages into {H}orn formulas},
booktitle = {Proceedings of {G}and{ALF} 2010},
editor = {{Montanari A.} and {Napoli M.} and {Parente M.}},
volume = {25},
series = {Electronic Proceedings in Theoretical Computer Science},
pages = {214--223},
abstract = {In recent work we have shown how it is possible to
define very precise type systems for object-oriented
languages by abstractly compiling a program into a Horn
formula f. Then type inference amounts to resolving a
certain goal w.r.t. the coinductive (that is, the
greatest) Herbrand model of f. Type systems defined in
this way are idealized, since in the most interesting
instantiations both the terms of the coinductive
Herbrand universe and goal derivations cannot be
finitely represented. However, sound and quite
expressive approximations can be implemented by
considering only regular terms and derivations. In
doing so, it is essential to introduce a proper
subtyping relation formalizing the notion of
approximation between types. In this paper we study a
subtyping relation on coinductive terms built on union
and object type constructors. We define an
interpretation of types as set of values induced by a
quite intuitive relation of membership of values to
types, and prove that the definition of subtyping is
sound w.r.t. subset inclusion between type
interpretations. The proof of soundness has allowed us
to simplify the notion of contractive derivation and to
discover that the previously given definition of
subtyping did not cover all possible representations of
the empty type. },
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/GandALF10.pdf},
keywords = {objects,types,coinduction},
year = 2010
}
@techreport{AnconaEtAl10,
author = {Ancona, D. and Corradi, A. and Lagorio, G. and
Damiani, F.},
title = {Abstract compilation of object-oriented languages into
coinductive {CLP}({X}): when type inference meets
verification},
institution = {Karlsruhe Institute of Technology},
note = {Formal {V}erification of {O}bject-{O}riented
{S}oftware. {P}apers presented at the {I}nternational
{C}onference, {J}une 28-30, 2010, {P}aris, {F}rance},
abstract = {We propose a novel general approach for defining
expressive type systems for object-oriented languages,
based on abstract compilation of programs into
coinductive constraint logic programs defined on a
specific constraint domain X called type domain. In
this way, type checking and type inference amount to
resolving a certain goal w.r.t. the coinductive (that
is, the greatest) Herbrand model of a logic program
(that is, a Horn formula) with constraints over a fixed
type domain X. In particular, we show an interesting
instantiation where the constraint predicates of X are
syntactic equality and subtyping over coinductive
object and union types. The corresponding type system
is so expressive to allow verification of simple
properties like data structure invariants. Finally, we
show a prototype implementation, written in Prolog, of
the inference engine for coinductive CLP(X), which is
parametric in the solver for the type domain X.},
booktitle = {Formal {V}erification of {O}bject-{O}riented
{S}oftware. {P}apers presented at the {I}nternational
{C}onference, {J}une 28-30, 2010, {P}aris, {F}rance},
editor = {Beckert, B. and March\'e, C.},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/FOVEOOS10-preproc.pdf},
keywords = {objects,types,coinduction},
publisher = {Karlsruhe},
series = {Karlsruhe Reports in Informatics (fr\"uher: Interner
Bericht. Fakult\"at f\"ur Informatik, Karlsruher
Institut f\"ur Technologie) ; 2010,13},
year = 2010
}
@inproceedings{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{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
}
This file was generated by bibtex2html 1.95.