Abstracts.2019.SizedTypes

MSc thesis: A Reflexive Graph Model of Sized Types

by Jannis Limperg

Sized types are a type-based termination checking mechanism for dependently typed languages. Compared to syntactic termination checkers, sized types make termination checking more modular and allow for an elegant treatment of coinductive and nested data types.

This thesis investigates λST, a simply-typed lambda calculus with sized types similar to those of Agda. The primary contribution is a relationally parametric reflexive graph model which suggests that the sizes of λST are irrelevant at runtime. The calculus and model are fully formalised in Agda (without sized types).