Data Types in Dependent Type Theory

Fredrik Nordvall Forsberg (University of Swansea, UK, Host: Tadeusz Litak)

3rd November 2011, 10:00 in ATT LT3

Martin-Löf's dependent type theory is both a foundational framework for constructive mathematics and a functional programming language with a very rich type system. Of course, we want this language to have a rich notion of data structure as well. I will review some classes of data types (indexed inductive types, inductive-recursive types, inductive-inductive types, ...) that one can add to dependent type theory, and how a certain formalisation in type theory naturally gives rise to generic programming. The talk will be aimed at a general audience.