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