Department of Computer Science faculty candidate Carlo Angiuli will give a technical presentation on March 1, 2023, at 1 p.m., in Fisher Hall, Room 132, and via Zoom.
Talk Title: Homotopy and the foundations of formal verification
Talk Abstract: Dependent type theory is an expressive type system that lies at the heart of many interactive theorem provers, tools for writing machine-checked proofs of program correctness. In recent years, researchers in the emerging field of homotopy type theory have uncovered surprising connections between dependent type theory and a branch of mathematics known as homotopy theory.
In this talk, I will show how theoretical ideas from homotopy type theory address shortcomings in the practice of formal verification. First, I will discuss how homotopy type theory lets us deduce representation independence theorems stating that two implementations of an abstract interface can be exchanged freely, provided they have equivalent input/output behavior. These theorems do not hold in traditional theorem provers, but can be leveraged to provide modular techniques for verifying data structures. Then, I will present Cartesian cubical type theory, a dependent type theory which reconstructs key features of homotopy type theory in the type system of a functional programming language. My collaborators and I have developed several prototype implementations of Cartesian cubical type theory, and a closely-related theory has been implemented at scale in the Agda programming language; experiments indicate that these systems are significantly easier to use than earlier implementations of homotopy type theory.
Speaker Bio: Carlo Angiuli is a postdoctoral fellow at Carnegie Mellon University, where he obtained his PhD in 2019 under the supervision of Robert Harper. His research interests are in programming languages and formal verification, with an emphasis on dependent type theory and its connections with mathematics and logic. His work has won the School of Computer Science Distinguished Dissertation Award at CMU and the Best Paper Award by Junior Researchers at FSCD.