Effective Type-driven Development for Graded Modal Types

在现代编程语言中，跟踪资源使用变得越来越重要，需要仔细监控内存和带宽等数量。此外，敏感地处理私人数据也同样重要，避免无意中泄露密码和银行信息等资源。验证编程语言属性的主要方法是使用类型系统。总的来说，这项工作试图使用类型系统来推理资源使用情况。实现这一点的一种基于类型的策略是使用分级模式类型的统一框架，该框架可以在单个类型理论中捕获各种资源分析。分级类型的方法正在迅速成为编程语言理论和实践中的流行范例，为编程语言(和语义)增加了细粒度分析所需的信息。最近，Orchard等人开发了语言颗粒。用于尝试使用分级模式类型进行最终用户编程。到目前为止，分级的模式类型已经被证明在程序推理方面是强大的，但它们给程序员带来了巨大的额外认知负担。这个博士项目将寻求使使用这种类型系统的编程更有效，使用户能够更容易地利用分级模式类型的力量，同时仍然保留编程的标准模型。一个潜在的工作途径是探索一种配套的表层语言，它允许隐式使用“分级”和“分级的模式类型”，从而使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.