An Agda formalisation of the transitive closure of block matrices
We define a block based matrix representation in Agda and lift various algebraic structures (semi-near-rings, semi-rings and closed semi-rings) to matrices in order to verify algorithms that can be implemented using the closure operation in a semi-ring.
Sun 18 Sep
|17:00 - 17:20|
Oleg KiselyovTohoku University
|17:20 - 17:40|