Vinh-Kha Le: Why is equality like a path? HoTT takes on proofs as programs. , April 2, 2019
|
Vinh-Kha Le will give the math table talk next Tuesday (April 2nd). His
title and abstract are below. Title: Why is equality like a path? HoTT takes on proofs as programs. Abstract. Homotopy theory, in the setting of algebra and topology, is nearly 200 years old. In that time, the field has evolved and matured a vast library of techniques. In that time, mathematicians also realized that those techniques could be applied to areas outside of topology. In this talk, we will discuss homotopy theory as it is applied to type theory, the area of logic and computer science that concerns itself with formal systems of proofs and programming languages. This so-called homotopy type theory (HoTT) emerged in the early 2000s partly as a method for automated proof checking. HoTT interprets proofs of theorems as points in spaces and proofs of equality as paths between points. Under this interpretation, it is possible to port over techniques from homotopy theory to resolve problems in type theory and vice versa. In particular, HoTT can translate mathematical proofs into a programming language such that valid proofs correspond to valid programs. A computer can then check proofs by running the corresponding programs. This talk will go over the general ideas of HoTT with minimal technicality. Any details provided will be presented accessibly. No prerequisites, though a basic understanding of proofs and programs is suggested. |