One Really HoTT Summer

Pun intended. This summer, I had the distinct opportunity of working with Prof. Amr Sabry at Indiana University (IU) Bloomington on the various applications of homotopy type theory (HoTT). Aside from being a foundation of mathematics, HoTT has illuminated many deep connections between computation, topology, and logic. Embedded below is the report I wrote which explains how we used HoTT to model the reversible programming paradigm and why that’s cool. You can also run it in Agda using the Literate Agda file! Plus, I might get to synthetic proofs of various basic results in homotopy theory in a later post.

The results in this report are formalized in Agda, one of the many proof assistants out there. Aside from the math I learned, the force of verified mathematics and software engineering is something that I’ve come to appreciate. Once you’ve seen the light that shines upon correct proofs and software, it’s hard not to go down the rabbit hole. I think I’ll be down there for a while, since my current projects have to do with proof assistant tooling.

Of course, this post is incomplete without a plug for IU Bloomington’s Research Experience for Undergraduates (REU) in Mathematics, the program under which I worked. It’s one of the oldest math REUs in existence (if not the oldest) and is one of the few left that focuses on pure mathematics, and with this project, the foundations of computing. Rarely is such a fulfilling experience available to aspiring researchers, so go forth and apply!