License
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2010.401
URN: urn:nbn:de:0030-drops-26661
URL: http://drops.dagstuhl.de/opus/volltexte/2010/2666/
Go to the corresponding Portal


Zantema, Hans ; Raffelsieper, Matthias

Proving Productivity in Infinite Data Structures

pdf-format:
Document 1.pdf (219 KB)


Abstract

For a general class of infinite data structures including streams, binary trees, and the combination of finite and infinite lists, we investigate the notion of productivity. This generalizes stream productivity. We develop a general technique to prove productivity based on proving context-sensitive termination, by which the power of present termination tools can be exploited. In order to treat cases where the approach does not apply directly, we develop transformations extending the power of the basic approach. We present a tool combining these ingredients that can prove productivity of a wide range of examples fully automatically.

BibTeX - Entry

@InProceedings{zantema_et_al:LIPIcs:2010:2666,
  author =	{Hans Zantema and Matthias Raffelsieper},
  title =	{{Proving Productivity in Infinite Data Structures}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{401--416},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Christopher Lynch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2666},
  URN =		{urn:nbn:de:0030-drops-26661},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.RTA.2010.401},
  annote =	{Keywords: Productivity, infinite data structures, streams}
}

Keywords: Productivity, infinite data structures, streams
Seminar: Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Issue Date: 2010
Date of publication: 06.07.2010


DROPS-Home | Fulltext Search | Imprint Published by LZI