Sites Inria

Version française

Research Teams' Seminar

Prosecco Seminar: Indexed Inductive Types

© INRIA Sophie Auvin - P comme Protocole

Indexed inductive types are a feature of most languages based on dependent types. So far, they have only been described as schematic extensions of a type theory or as being instances of the very semantically oriented definition of (indexed) W-types. 

  • Date : 23/10/2019
  • Place : Room Jacques Louis Lions 2
  • Guest(s) : Jakob von Raumer (University of Nottingham)

We present an intrinsic type-theoretic syntax which can be used to specify indexed inductive types.

We present the semantics of this syntax, show that it is internalizable in any language supporting indexed W-types and, using this internalization, prove the existence of indexed inductive types in such languages.

Keywords: Indexed Inductive Types Research Seminar Prosecco Inria de Paris Science