We are happy that Mukesh Tiwari joined Swansea University recently. Today he will give a talk as a part of out theory seminar series:
Formalizing linear algebra over semirings
"Linear algebra over real numbers (field algebraic structure) is a powerful mathematical tool for understanding and solving a wide range of computing problems. Nonetheless, it is not without its limitations, as a specific implementation tailored to one problem may not be readily applicable to solve another, i.e., it does not generalise well. In this talk, I will present a certified implementation of several linear algebraic methods such as matrix addition, matrix multiplication, matrix exponentiation, and matrix formal power series (Kleene star) over semiring in the Coq theorem prover. Semiring is a weaker structure than field and therefore can accommodate more applications and I will demonstrate the flexibility of this implementation by instantiating the abstract operators of semiring with concrete mathematical operators and depending on the instantiation, it can solve wide range of problems, ranging from voting, optimisation, social network, etc. The Coq formalisation is available on GitHub [1]"
