## Verification of redecoration for infinite triangular matrices in Coq

Institut de Recherche en Informatique de Toulouse

Université Paul Sabatier (Toulouse 3)

Thursday, 13 September 2012, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

**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. Both kinds of families are fully supported since the version
8.1 of the Coq theorem proving environment, released in 2007.

Still today, reasoning about nested coinductive types in Coq
constantly faces challenges due to the guardedness condition that
imposes syntactic conditions on otherwise well-defined corecursive
definitions and proofs. In this talk, we concentrate on results that
could smoothly be obtained by rather modest generalizations of the
statements that could not directly be proven by coinduction.

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

We then validate the original algorithm against another
visualization of the triangles, provably equivalent to the first
one. It is then 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.

(Joint work with Ralph
Matthes.)

Celia Picard's visit to Tallinn is supported by the ETF/Egide
Parrot programme.

Tarmo Uustalu

Last update 19.9.2012