Matthes, Ralph ;
Picard, Celia
Verification of redecoration for infinite triangular matrices using coinduction
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 wellknown 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 typetheoretic 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 = {5569},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897491},
ISSN = {18688969},
year = {2013},
volume = {19},
editor = {Nils Anders Danielsson and Bengt Nordstr{\"o}m},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/3900},
URN = {urn:nbn:de:0030drops39001},
doi = {10.4230/LIPIcs.TYPES.2011.55},
annote = {Keywords: nested datatype, coinduction, theorem proving, Coq}
}
2013
Keywords: 

nested datatype, coinduction, theorem proving, Coq 
Seminar: 

18th International Workshop on Types for Proofs and Programs (TYPES 2011)

Issue date: 

2013 
Date of publication: 

2013 