An agda formalisation of the transitive closure of block matrices (extended abstract).

Adam Sandberg Eriksson, Patrik Jansson

Browse the full ICFP paper archive.