Verification of redecoration for infinite triangular matrices using coinduction

Ralph Matthes & Celia Picard
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...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.