Programming languages for scalable incremental computation and advanced gradual typing

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

Scalable incremental computation******Software 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 typing******Advances 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.******Impact******By 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.