Effective Type-driven Development for Graded Modal Types

点击翻译按钮获取中文摘要

In modern programming languages, tracking resource usage is increasingly important, with quantities such as memory and bandwidth needing to be carefully monitored. Furthermore, it is equally important to handle private data sensitively, and avoid leaking resources such as passwords and banking information inadvertently. A dominant approach for verifying properties of programming languages is the use of a type system. Broadly, this work seeks to use type systems for reasoning about resource use. One type-based strategy for doing this is to use the unified framework of graded modal types, which can capture various kinds of resource analysis in a single type theory. The approach of graded types is fast becoming a popular paradigm in programming language theory and practice, augmenting programming languages (and semantics) with information required for fine-grained analysis. Recently, the language Granule was developed by Orchard et al. for experimenting with end-user programming with graded modal types. So far, graded modal types have been shown to be powerful for reasoning about programs, but they place a large additional cognitive burden on the programmer. This PhD project will seek to make programming with such type systems more effective, enabling users to more easily exploit the power of graded modal types whilst still retaining a standard model of programming. One potential avenue of work is to explore a companion surface-level language which allows 'grades' and 'graded modal types' to be used implicitly, so that programs in Granule more closely resemble standard functional programs. This would make Granule more user-friendly and allow for it to be used in a wider range of contexts, so that the power and precision of graded modal types can benefit a broader audience. Other avenues of exploration towards this goal include type inference, assistive programming technologies, interactive compilation techniques, and program synthesis. This project will consider applications to reasoning about privacy and confidentiality of data from within the programming language. This has the potential to transform the way programming languages are used to guarantee safety properties of critical software.