Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: Fredrik Nordvall Forsberg: Inductive-inductive definitions in Type Theory

LFCS Seminar: Fredrik Nordvall Forsberg: Inductive-inductive definitions in Type Theory

— filed under:

Fredrik Nordvall Forsberg, University of Strathclyde

What
  • LFCS Seminar
When Apr 28, 2015
from 04:00 PM to 05:00 PM
Where 4.31/4.33
Add event to calendar vCal
iCal

Abstract:

 Martin-Lö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

 inductive-inductive definitions. I will give several examples, and

 

 discuss their meta-theory.

Document Actions