Quantitative Program Reasoning with Graded Modal Types: Most programming languages treat data as infinitely copiable, arbitrarily discardable, and universally unconstrained. However, this overly abstract view is naïve and can lead to software errors. For example, some data encapsulates resources subject to protocols (e.g., file and device handles, channels); some data has confidentiality requirements and thus should not be copied or communicated arbitrarily. Dually, some programs have non-functional properties (e.g., execution time) dependenton data (e.g., on its size). Thus, the reality is that some data acts as a resource, subject to constraints. In this paper we present Granule, a typed functional language that embeds a notion of data as a resource into the type system in a way that can be specialised to different resource and dataflow properties. Granule’s type system combines linear types, indexed types (lightweight dependent types), and graded modal types to enable novel quantitative reasoning. Link