Dependent types have been pioneered by Per Martin-Löf as a formal framework to carry out intuitionistic mathematics. The major feature of dependent type theories is that definitions, computations and proofs are given in the same language. Moreover, correctness checking of proofs amounts to type-checking, which is well understood. The latter requires though that the associated reduction relation is strongly normalising on all terms a type can depend on, so to obtain an actual algorithm for type checking.

Most formal type systems with dependent types allow the use of inductive types, among other base types, to carry out actually interesting mathematics. Inductive types have been studied vastly in this context, and we know precisely how to incorporate them into dependent type systems with a strongly normalising reduction relation. On the other hand, in computer science, but also in mathematics, we frequently encounter (possibly) infinite computations that are nevertheless well-defined. The concept that emerged to accommodate infinite computations is that of coinductive types. The really interesting examples arise though from the mix of inductive and coinductive types, which has hardly been investigated in the context of dependent type theories.

In this talk, I will present first a category theoretical perspective on dependent type theories that are solely based on mixed inductive-coinductive types. Such theories allow us to encode intuitionistic logic as inductive or coinductive types. Vice versa, we also show that dependent inductive-coinductive types can be constructed in categories with enough structure just from non-dependent inductive types. We then use this high level perspective to set up a syntactic calculus with inductive-coinductive types. For this calculus we will prove that its associated reduction relation preserves types and is strongly normalising. Finally, if time permits, we might discuss future directions of how to internalise bisimilarity on coinductive types into the calculus, while retaining decidable type checking.

The category theoretical view is based on a paper I presented at FICS 2015, whereas the calculus and its properties are joint work with Herman Geuvers presented at LICS 2016.