Research Teams' Seminar
Prosecco Seminar: Indexed Inductive Types
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.
- Date : Wednesday, October 23rd 2019
- Hour : 2pm
- Place: Inria de Paris, Room Salle Jacques Louis Lions 2