Colloquium: Expressive Types

March 2, 2018 - 11:15am to 12:15pm
Institute for Advanced Study
Mechanical Engineering 212
Gopalan Nadathur

 BIOGRAPHY: Favonia (Kuen-Bang Hou) received their PhD in Computer Science from Carnegie Mellon University and is a postdoctoral member of Institute for Advanced Study, whose primary interest lies in making things more precise and reliable. In recent years, Favonia and their collaborators have been verifying important results in homotopy theory by computers, developing cubical computational type theory, and building the proof assistant RedPRL based on the newly developed type theory. They have also been working on property-based testing and compiler correctness in hopes of improving software quality.

ABSTRACT: Type theory is an effective language to express abstraction, and its development has been a major source of technical advances in formal reasoning. Over the years, I have been exploring new type theories and building new reasoning tools based on existing theories, and my research has led to new insights in both mathematics and programming.

In this talk, I will use my work in homotopy type theory, cubical computational type theory and parametric polymorphism to demonstrate how foundational improvements in type theory can grant us unforeseen expressiveness, and how we might still underestimate the potential of existing type theories. I will also discuss some new research directions that will reveal more power of type theory in the context of programming.