English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

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 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.  <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 type-theoretic language. Thus, it should be  accessible without any specific knowledge about Coq

Verification of redecoration for infinite triangular matrices using coinduction