LFCS Seminar: Fredrik Nordvall Forsberg: Inductiveinductive definitions in Type Theory
Fredrik Nordvall Forsberg, University of Strathclyde
What 


When 
Apr 28, 2015 from 04:00 PM to 05:00 PM 
Where  4.31/4.33 
Add event to calendar 
vCal iCal 
Abstract:
MartinLöf's dependent type theory can be seen as 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 describe one class of such data types
which I studied during my PhD, where a type A is formed inductively,
simultaneously with a second type B : A > Type which depend on it.
Both types are formed inductively, hence we call such definitions
inductiveinductive definitions. I will give several examples, and
discuss their metatheory.