Programming languages for scalable incremental computation and advanced gradual typing

用于可扩展增量计算和高级渐进类型的编程语言

• 批准号: RGPIN-2018-04352
• 负责人: Dunfield, Jana
• 金额: $ 2.4万
• 依托单位: Queen's University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750616
• 关键词: Programming; languages; scalable; incremental; computation

Scalable incremental computationSoftware defects are everywhere. Slow software is also defective: a right answer is no better than a wrong one, if it takes too long. Many software systems receive similar inputs over time: compilers are often re-run after changing a single line of code. These systems can reuse previous work through incremental computation (IC).However, reusing work is difficult when the dependencies between subcomputations are subtle. Programming languages for IC automate reuse by extending languages and compilers: guided by program annotations, the compiler incrementalizes the program. This approach can achieve asymptotic speedups without extensive programmer effort.Existing approaches, however, do not work for larger systems. Our first long-term goal is to enable automatic incrementalization of large software systems, such as compilers.To achieve this goal, we will design and implement a language and semantics of incremental programs with complex structure, describing the behaviour of larger incremental systems. To understand higher-level behaviour and guide programmer understanding, we will design and implement type systems that check invariants of incremental programs.Advanced gradual typingAdvances in formal verification have led to fully verified software, such as the CompCert C compiler and the seL4 OS kernel. The importance of such systems justifies the expense of verifying them. For most applications, however, requirements change often and defects' consequences are less severe. Thus, full verification will probably remain too expensive for most software.Refinement typing occupies the middle ground, ruling out large categories of defects with less developer investment of training and time. However, refinement typing shares a drawback of traditional type systems: either the entire program type-checks, or it doesn't. Making typing more powerful increases the burden on programmers who have time to verify only the most critical parts of their software.Gradual typing allows different parts of a program to be checked against different levels of typing. Our second long-term goal is to develop tools that enable language designers to build gradually typed languages easily.Thus, we will develop general mechanisms for gradual typing that allow programmers to choose when and where to pay the price for different levels of typing guarantees.We will combine both long-term goals through gradual typing for large incremental systems.ImpactBy making incrementality easier to achieve, scalable IC will soften the tradeoff between performance and maintainability. Advanced gradual typing will enable programmers to choose a practical amount of verification at a fine-grained level.The proposed research will prepare 3 PhD, 2 MSc and 3 undergraduate students for successful careers in both academic research and industry.

可扩展的增量计算软件缺陷无处不在。慢软件也有缺陷：如果花费太长，正确的答案就不会比错误的答案更好。随着时间的推移，许多软件系统会收到类似的输入：更改一行代码后，编译器通常会重新运行。这些系统可以通过增量计算（IC）重复使用以前的工作。但是，当子分组之间的依赖关系微妙时，重复使用工作就很难。通过扩展语言和编译器来进行IC自动重复使用的编程语言：在程序注释的指导下，编译器会增加程序。这种方法可以在无需大量程序员努力的情况下实现渐近的加速。但是，使用的方法不适用于较大的系统。我们的第一个长期目标是启用大型软件系统（例如编译器）的自动增量化。为了实现此目标，我们将设计和实施具有复杂结构的增量程序的语言和语义，描述了较大的增量系统的行为。为了了解更高级别的行为和指导程序员的理解，我们将设计和实施类型的系统，以检查增量程序的不变性。在正式验证中进行了渐进的逐渐键入活动，导致了完全验证的软件，例如Compcert C Compiler和SEL4 OS内核。此类系统的重要性证明了验证它们的费用。但是，对于大多数应用程序，需求经常发生变化，缺陷的后果也不那么严重。因此，对于大多数软件而言，全面验证可能仍然太昂贵了。进行键入占据了中间立场，排除了大量的缺陷，而开发人员的培训和时间投资较少。但是，精炼键入分型具有传统类型系统的缺点：整个程序类型检查，或者没有。使键入更强大会增加有时间仅验证其软件最关键部分的程序员的负担。级别键入允许对程序的不同部分进行检查，以相对于不同级别的键入。我们的第二个长期目标是开发工具，使语言设计师能够轻松地构建逐渐键入的语言。因此，我们将开发逐渐键入的一般机制，使程序员可以选择何时以及在何时付费不同的型号保证，我们将通过逐渐键入大量的增量系统来逐步键入，以使递增性保持稳定性，从而可以轻松地保持稳定性。高级渐进式键入将使程序员能够在细粒度的水平上选择实用的验证。拟议的研究将准备3个博士学位，2名MSC和3名本科生，以在学术研究和行业中成功职业。