Fiat is a Coq framework for refining specifications into efficient programs on which my work will be based. Although currently there are already many platforms to process linear algebra formulas, the users usually cannot choose the way they want to process the formula. In some cases, the user might be able to change the open-source code to support more powerful calculations. But after the change, the code isn’t guaranteed to still be be correct (and even before the change, the code isn’t proven to be correct). In contrast, using Fiat to do linear algebra can help us overcome this difficulty. My research project involves working on this platform and focusing especially on formulas that people are interested in.

I am participating in SuperUROP because I want to see how real research in computer science is like. I have been working with Professor Chlipala during the past spring and was quite interested in the area he is working on. I hope through this SuperUROP experience I can create something that’s useful and guaranteed to be true.