@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -c 'keywords : "corecursion"' /home/davide/latex/bibinputs/allMine.bib}}
@comment{{This file has been generated by Pybliographer}}
@article{AnconaCOMLAN13,
institution = {{DIBRIS - Universit{\`{a}} di Genova}},
keywords = {{coinduction,corecursion}},
note = {{Extended version of \url{http://www.disi.unige.it/person/AnconaD/papers/Conferences_abstracts.html#AnconaSAC12}{SAC 2012}}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/COMLAN13.pdf},
author = {Ancona, D.},
title = {{Regular corecursion in Prolog}},
journal = {{Computer Languages, Systems \& Structures}},
volume = {39},
number = {4},
pages = {142-162},
year = {2013},
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 a new interpreter to solve the problem of
non-terminating failure as experienced with the
standard semantics of coinduction (as supported, for
instance, in SWI-Prolog). Another problem with the
standard semantics is that predicates expressed in
terms of existential quantification over a regular term
cannot directly defined by coinduction; to this aim, we
introduce finally clauses, to allow more flexibility in
coinductive definitions. Then we investigate the
possibility of annotating arguments of coinductive
predicates, to restrict coinductive definitions to a
subset of the arguments; this allows more efficient
definitions, and further enhance the expressive power
of coinductive Prolog. We investigate the effectiveness
of such features by showing different example programs
manipulating several kinds of cyclic values, ranging
from automata and context free grammars to graphs and
repeating decimals; the examples show how computations
on cyclic values can be expressed with concise and
relatively simple programs. The semantics defined by
these vanilla meta-interpreters are an interesting
starting point for a more mature design and
implementation of coinductive Prolog. }
}
@inproceedings{AZ_FTfJP13,
booktitle = {{Formal techniques for Java-like programs (FTfJP13)}},
keywords = {{objects, coinduction, corecursion}},
ftp = {ftp://ftp.disi.unige.it/person/AnconaD/AZ-FTfJP13.pdf},
author = {Ancona, D. and Zucca, E.},
title = {{Safe Corecursion in coFJ}},
pages = {2:1--2:7},
year = {2013},
abstract = {In previous work we have presented coFJ, an extension
to Featherweight Java that promotes coinductive
programming, a sub-paradigm expressly devised to ease
high-level programming and reasoning with cyclic data
structures. The coFJ language supports cyclic objects
and regularly corecursive methods, that is, methods
whose invocation terminates not only when the
corresponding call trace is finite (as happens with
ordinary recursion), but also when such a trace is
infinite but cyclic, that is, can be specified by a
regular term, or, equivalently, by a finite set of
recursive syntactic equations. In coFJ it is not easy
to ensure that the invocation of a corecursive method
will return a well-defined value, since the recursive
equations corresponding to the regular trace of the
recursive calls may not admit a (unique) solution; in
such cases we say that the value returned by the method
call is undetermined. In this paper we propose two new
contributions. First, we design a simpler construct for
defining corecursive methods and, correspondingly,
provide a more intuitive operational semantics. For
this coFJ variant, we are able to define a type system
that allows the user to specify that certain
corecursive methods cannot return an undetermined
value; in this way, it is possible to prevent unsafe
use of such a value. The operational semantics and the
type system of coFJ are fully formalized, and the
soundness of the type system is proved. }
}
@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{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)},
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
}
This file was generated by bibtex2html 1.98.