CoGITARe : "Combining Graded and Intersection Types for the Analyses of Resources"
Funded by ANRJCJC
Period of activity : 2019-2022
Official and associated members : Jaime Arias, Flavien Breuvart, Jérôme Féret, Dan Ghica, Jean-Vincent Loddo, Giulio Manzonetto, Damilano Mazza, Yann Régis-Gianas, Thomas Seiller
Summary :
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 techniques, enabling in particular the analysis of {\bf 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.