Matthes, Ralph and Picard, Celia Verification of redecoration for infinite triangular matrices using coinduction. (2013) In: International Workshop on Types and Proofs for Programs  TYPES 2011, 8 September 2011  11 September 2011 (Bergen, Norway).

(Document in English)
PDF (Author's version)  Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 459kB 
Official URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2011.55
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. <p> 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. <p> 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. <p> 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.
Item Type:  Conference or Workshop Item (Paper) 

Additional Information:  Thanks to Schloss Dagstuhl editor. The definitive version is available at http://www.proceedings.com/17839.html 
HAL Id:  hal01143261 
Audience (conference):  International conference proceedings 
Uncontrolled Keywords:  
Institution:  Université de Toulouse > Institut National Polytechnique de Toulouse  INPT (FRANCE) French research institutions > Centre National de la Recherche Scientifique  CNRS (FRANCE) Université de Toulouse > Université Toulouse III  Paul Sabatier  UPS (FRANCE) Université de Toulouse > Université Toulouse  Jean Jaurès  UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole  UT1 (FRANCE) 
Laboratory name:  
Statistics:  download 
Deposited By:  IRIT IRIT 
Deposited On:  17 Apr 2015 09:22 
Repository Staff Only: item control page