License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2011.55
URN: urn:nbn:de:0030-drops-39001
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/3900/
Go to the corresponding LIPIcs Volume Portal

Matthes, Ralph ; Picard, Celia

Verification of redecoration for infinite triangular matrices using coinduction

pdf-format:
6.pdf (0.4 MB)

Abstract

Finite triangular matrices with a dedicated type for the diagonal
elements can be profitably represented by a nested data type, i. e., a
heterogeneous family of inductive data types, while infinite
triangular matrices form an example of a nested coinductive type,
which is a heterogeneous family of coinductive data types.

Redecoration for infinite triangular matrices is taken up from
previous work involving the first author, and it is shown that
redecoration forms a comonad with respect to bisimilarity.

The main result, however, is a validation of the original algorithm
against a model based on infinite streams of infinite streams. The
two formulations are even provably equivalent, and the second is
identified as a special instance of the generic cobind operation
resulting from the well-known comultiplication operation on streams
that creates the stream of successive tails of a given stream. Thus,
perhaps surprisingly, the verification of redecoration is easier for
infinite triangular matrices than for their finite counterpart.

All the results have been obtained and are fully formalized in the
current version of the Coq theorem proving environment where these
coinductive datatypes are fully supported since the version 8.1,
released in 2007. Nonetheless, instead of displaying the Coq
development, we have chosen to write the paper in standard
mathematical and type-theoretic language. Thus, it should be
accessible without any specific knowledge about Coq.

BibTeX - Entry

@InProceedings{matthes_et_al:LIPIcs:2013:3900,
  author =	{Ralph Matthes and Celia Picard},
  title =	{{Verification of redecoration for infinite triangular matrices using coinduction}},
  booktitle =	{18th International Workshop on Types for Proofs and Programs (TYPES 2011)},
  pages =	{55--69},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-49-1},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{19},
  editor =	{Nils Anders Danielsson and Bengt Nordstr{\"o}m},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/3900},
  URN =		{urn:nbn:de:0030-drops-39001},
  doi =		{10.4230/LIPIcs.TYPES.2011.55},
  annote =	{Keywords: nested datatype, coinduction, theorem proving, Coq}
}

Keywords: nested datatype, coinduction, theorem proving, Coq
Collection: 18th International Workshop on Types for Proofs and Programs (TYPES 2011)
Issue Date: 2013
Date of publication: 21.01.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI