Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / WS 2012/13 / Oberseminar / Frederik Forsberg, Internalizing inductive-inductive definitions in Martin-Löf Type Theory


Inhaltsbereich

Frederik Forsberg, Internalizing inductive-inductive definitions in Martin-Löf Type Theory

TCS Oberseminar, Dienstag(!) 27.11.2012 14:15 L109
Wann 14:15 15:15 27.11.2012
von bis
Wo L109
Termin übernehmen vCal
iCal

Fredrik Forsberg
Internalizing inductive-inductive definitions in Martin-Löf Type Theory

Martin-Löf's dependent type theory can be seen both as a foundational framework for constructive mathematics, and 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, where a type A is formed inductively, simultaneously with a second type B : A -> Type which depend on it. Since both types are formed inductively, we call such definitions inductive-inductive definitions.
Examples of inductive-inductive definitions, e. g. sorted lists, Conway's surreal numbers and the syntax of dependent type theory,will be given, in order to demonstrate the usefulness of the notion. I will then sketch a finite axiomatization of the theory, and if time permits discuss a categorical semantics in a category of dialgebras.

Artikelaktionen


Funktionsleiste