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 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
17:00 - 18:00
|Parameterized Extensible Effects and Session Types|
Oleg Kiselyov Tohoku University
|An Agda formalisation of the transitive closure of block matrices|