Graded Modal Dependent Type Theory

TL;DR

Graded Modal Dependent Type Theory (GrTT) introduces a flexible framework for analyzing data flow within dependent types, enabling advanced reasoning about program properties and optimizing type checking.

Contribution

This work presents the first dependent type theory with a general, parameterizable data flow analysis, integrating grading into the dependent type setting.

Findings

Successfully formalized GrTT and studied its metatheory.

Demonstrated case studies applying GrTT to program reasoning.

Implemented the theory and applied grading to optimize type checking.

Abstract

Graded type theories are an emerging paradigm for augmenting the reasoning power of types with parameterizable, fine-grained analyses of program properties. There have been many such theories in recent years which equip a type theory with quantitative dataflow tracking, usually via a semiring-like structure which provides analysis on variables (often called `quantitative' or `coeffect' theories). We present Graded Modal Dependent Type Theory (GrTT for short), which equips a dependent type theory with a general, parameterizable analysis of the flow of data, both in and between computational terms and types. In this theory, it is possible to study, restrict, and reason about data use in programs and types, enabling, for example, parametric quantifiers and linearity to be captured in a dependent setting. We propose GrTT, study its metatheory, and explore various case studies of its use in reasoning about programs and studying other type theories. We have implemented the theory and highlight the interesting details, including showing an application of grading to optimising the type checking procedure itself.