A Reflexive Graph Model of Sized Types

Abstract

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. Its primary contribution is a relationally parametric denotational semantics for λST in the form of a reflexive graph model. In this model, sizes are irrelevant: they do not affect the result of any computations. The calculus and model are fully formalised in Agda (without sized types).