Graded Modal Type Theory, Formalized

Abstract

A graded modal type theory equips a type theory with a semiring of grades, which enables encoding additional information of some kind. A typical application of such a system is to encode quantitative information, specifically how many times variables are used or referenced at runtime. Concrete examples include erasure or linear types. In this thesis, we present such a type theory with dependent types, designed primarily with encoding quantitative information in mind. The theory supports Π-types, Σ-types, unit, and empty types, as well as a hierarchy of universes. It also supports natural numbers, and special attention is given to establishing a method for counting variable uses for the recursive eliminator of this type. We prove some key meta-theoretical results for this system, as well as two main correctness results. Firstly, we show correctness for erasure in the sense that it is safe to remove erased information during compilation without affecting the result of evaluation. Secondly, we show that the system is capable of correctly tracking how many times variables should be referenced through an abstract machine in which heap lookups (corresponding to variable references) are tracked. The thesis is accompanied by an Agda formalization in which the results have been mechanized.