Download on the App Store Open In Castro
Podcast artwork

05/29/21: Homotopy Type Theory 101 with Carlo Angiuli

Boston Computation Club

June 9, 2021

64 minutes

Carlo is a postdoc in the Computer Science Department at Carnegie Mellon University, where he received a Ph.D. under Robert Harper. He previously studied at Indiana University Bloomington, where he received a B.S. in Mathematics and in Computer Science.  Today Carlo joined us to discuss Homotopy Type Theory, a new foundations for mathematics based on a recently-discovered connection between Homotopy Theory and Type Theory.  Carlo explains intuitively what Homotopy Type Theory is and how it is used, and then goes over various possible implementations of Homotopy Type Theory in a theorem-proving environment such as Coq.  Finally, he fields questions on Homotopy Type Theory, theorem-proving, and other topics from the Boston Computation Club audience.

Or Listen Elsewhere

Listen On Apple Podcasts
Listen In Pocket Casts
Listen In Overcast
Subscribe to RSS