Combining Graded and Intersection Types for the Analyses of Resources – CoGITARe

Type systems are used to automatically check security properties of large programs. This project will extend typing methodology to a large panel of properties currently unreachable by state-of-the-art tech-niques, enabling in particular the analysis of quantitative properties of programs.

We will develop a way to keep track of the extensional information inside types in order to perform the whole static analysis at the level of types. For this purpose, we will combine two (re)emerging type systems, namely graded types and intersection type systems, with the well established techniques from the field of abstract interpretation such as widening.

Graded type systems formally embed a first order structure within types, while intersection types will help to circumvent the unconditional non-compositionality of fine grained resource analyses. This is how we plan to tackle the long running problem of applying abstract interpretation result in functional
programming.