A University of Iowa researcher has been awarded $1.2 million from the National Science Foundation to develop a method to unify how researchers write, verify, and reuse proofs in mathematics and computer science. 

J. Garrett Morris, assistant professor in the Department of Computer Science, is the lead investigator on the four-year project, the goal of which is to improve how researchers verify complex ideas in mathematics and programming languages. In particular, Morris’ research focuses on creating a framework that makes it easier to understand and computerize the structure of proofs and logical rules used in any other setting. 

“Once you go from a proof being just an argument on paper to it being a piece of software, it becomes easier to collaborate,” Morris says. “I can say, ‘You work on these pieces, I’ll work on those,’ and I’m not proofreading your work. I’m just asking, does the machine check it? That’s a way forward.” 

In computer science and mathematics, researchers use specialized software tools known as theorem provers to write and check proofs — a way of showing a statement is true by using logic and previously proven facts that have been vetted by the research community. 

However, reusing proofs across computer systems can be challenging. Different theorem provers follow distinct logics and represent common structures differently. The tools also have different formats, languages, and ways of representing proofs. Because of these differences, a proof made in one system might not translate to another. 

To address these issues, Morris wants to create a framework that makes the internal structure of proofs and data more visible and transferable. One innovation would include introducing row types — which describe the structure of data within the framework itself — to theorem proving. That could simplify how systems identify when parts of a proof can be reused — even if they come from different theorems or use various logical rules — allowing the transition of valid results in one system to another. 

Once developed, the logical framework could benefit any sector where the correctness, safety, and reliability of software are crucial. While industries such as the military, avionics, and finance already use similar applications, this unified framework could continue to benefit those sectors and others. 

“It matters whether your software does the things that you want it to do, and this work will build on significant efforts towards proving programs correct in those areas,” Morris says.