Effective Type-driven Development for Graded Modal Types

在现代编程语言中，跟踪资源使用情况变得越来越重要，需要仔细监控内存和带宽等数量。此外，敏感地处理私人数据，避免无意中泄露密码和银行信息等资源也同样重要。验证编程语言属性的主要方法是使用类型系统。总的来说，这项工作试图使用类型系统来推理资源的使用。一种基于类型的策略是使用分级模态类型的统一框架，它可以在单一类型理论中捕获各种资源分析。分级类型的方法正在迅速成为编程语言理论和实践中的一种流行范式，用细粒度分析所需的信息增强了编程语言（和语义）。最近，Orchard等人开发了Granule语言，用于实验使用渐变模态类型的最终用户编程。到目前为止，分级模态类型已经被证明在程序推理方面很强大，但它们给程序员带来了很大的额外认知负担。这个博士项目将寻求使使用这种类型系统的编程更有效，使用户能够更容易地利用分级模态类型的力量，同时仍然保留标准的编程模型。一个潜在的工作途径是探索一种伴随的表面级语言，它允许隐式地使用“分级”和“分级模态类型”，从而使Granule中的程序更接近于标准的函数式程序。这将使Granule更加用户友好，并允许它在更广泛的上下文中使用，因此分级模态类型的功能和精度可以使更广泛的受众受益。实现这一目标的其他探索途径包括类型推断、辅助编程技术、交互式编译技术和程序合成。这个项目将考虑应用程序来推理的隐私和机密性的数据从编程语言。这有可能改变编程语言用于保证关键软件安全属性的方式。

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.