CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

An Agda formalisation of the transitive closure of block matrices (Extended Abstract)

Adam Sandberg Eriksson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
TyDe 2016 Proceedings of the 1st International Workshop on Type-Driven Development p. 2. (2016)
[Konferensbidrag, refereegranskat]

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.

Nyckelord: Dependent types, Linear Algebra



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2016-08-31. Senast ändrad 2016-08-31.
CPL Pubid: 240988

 

Läs direkt!

Lokal fulltext (fritt tillgänglig)

Länk till annan sajt (kan kräva inloggning)