Title: Proofgramming
Speaker: James (Jim) Fowler
Abstract: Computers are a popular tool for numeric calculations, but computers can also do calculations with proofs. In this introductory talk, we will use a computer as a "proof assistant" meaning that we will record definitions and theorems and, through an interactive dialogue with the computer in the language of type theory, prove some theorems.
Even if you aren't interested in formalizing some piece of mathematics, the ideas are interesting and broadly accessible: type theory provides a context where propositions (which may be true or false) and proofs and sets are all mathematical objects. For instance, a universally quantified theorem, proven constructively, becomes a function that can be applied to its inputs. A lemma is like a subroutine. Homotopy type theory goes farther, making an analogy between the equality of two objects and a path between those objects, so that some topological gadget like a "fibration" then has some type theoretic analogue.
