On Recursion in Graded Modal Type Theory

We present a graded modal type theory with recursion over natural numbers and prove formally in Agda that it handles resources correctly, in the sense that an abstract machine accesses resources the "correct" number of times. The theory is parametrized, and can for instance be instantiated with grades for erasure, linear types, or affine types. The correctness proof shows that our usage counting is sound. Our eliminator for natural numbers is flexible as it enables different resource-usage patterns and practical in the sense that it can be used both to define functions with expected usage counts for the arguments. Further, it can be used to encode other data types, using large elimination. Finally, we adapt our resource correctness proof to show correctness also for grades tracking information flow, in the form of a non-interference property.