A Reflexive Graph Model of Sized Types
Ladda ner
Typ
Examensarbete för masterexamen
Program
Publicerad
2020
Författare
Limperg, Jannis
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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).