Carlo Angiuli, assistant professor of Computer Science at the Luddy School of Informatics, Computing, and Engineering, has received a three-year, $449,387 grant from the Air Force Office of Scientific Research for his proposal, “Univalent Verification of Parameterized Structures.”
The project aims to develop new techniques using homotopy type theory to verify the correctness of functional data structures. It could lead to more efficient verification processes for functional data structures and improve techniques for the formal verification of critical software systems and large-scale mathematical proofs to ensure reliable and safe software systems.
“Carlo is one of the junior faculty members we recruited to the Computer Science department in 2023,” said Yuzhen Ye, Computer Science chair and professor of Informatics and Computer Science, “and I am glad that he has already secured a significant grant. This funding will enable him and his students to conduct impactful research with both theoretical and practical implications for programming languages and software verification.”
Angiuli said dependent type theory is used in the formal verification of computer programs and mathematical proofs, particularly in the development of correct-by-construction typed functional programs.
“Over the past 15 years,” he said, “a new interdisciplinary field known as homotopy type theory has emerged from surprising connections between dependent type theory, homotopy theory and higher category theory. That will lead to new theoretical insights in all three areas.”
Angiuli proposes to develop new foundational techniques for the formal verification of functional data structures in dependent type theory based on insights from homotopy type theory.
Computer scientists and mathematicians increasingly use proof assistants, which is software such as Cubical Agda that are designed to develop proofs on a computer and check that those proofs are correct.
Angiuli’s research will extend previous work on reasoning about complex data structures, building on the Structure Identity Principle and higher inductive types to ensure that the internal workings of a data structure don’t affect its overall behavior, and reduce the effort needed to verify data structures in the Cubical Agda proof assistant. It also will increase proof modularity by dividing complex verifications into smaller, reusable steps.
IU President Pamela Whitten said in a congratulatory letter that Angiuli’s “groundbreaking research has a major influence on not only the experiences of Indiana University students, but also the greater global community.” She said it ties into IU’s 2030 Strategic Plan to engage in high-impact research and creative activity, advance knowledge and improve the lives of people in the state of Indiana, and beyond.