The EECS Department welcomes Prof. Aaron Stump, Professor in Computer Science at The University of Iowa.

Stump will present a talk entitled "Marvels of Extrinsic Type Theory" on Friday, October 20 at 2:30 PM in Ford ITW Room.

Abstract: The form of type theory implemented in constructive theorem provers like Coq and Agda is *intrinsic*: type annotations are considered essential parts of expressions, and are not erased during formal reasoning. In this talk, I present some of the amazing things that are possible when one abandons this commitment to types as essential parts of terms, working instead in *extrinsic* type theory: terms are essentially just pure untyped lambda-calculus terms, and types make statements about their behavior. Using the theorem prover Cedille under development in my group, I will discuss surprising results such as: derivability of natural-number induction for pure lambda-encodings; more generally, derivability of induction for any functor; derivation of monotone recursive types; and derivability of constant-time coercions between isomorphic types like lists and vectors. All these constructs have been derived within the theory itself, where in other approaches they have been considered as additions that must be made to the theory. This shows that Cedille's type theory of Cedille is surprisingly expressive, despite being very compact: just the Calculus of Constructions plus a small handful of additional new constructs. The talk will not presuppose knowledge of type theory.

Bio: Prof. Aaron Stump is a full professor of Computer Science at The University of Iowa. He received his undergraduate degree from Cornell University in 1997, and PhD in Computer Science from Stanford in 2002. His current research focus is on type theory. He is the author of "Programming Language Foundations" (Wiley, 2013) and "Verified Functional Programming in Agda" (ACM Books, 2016).

Hosted by EECS Prof. Robby Findler