CAREER: Controlling Space Properties of Higher-Order Typed Programs

高阶、类型化、函数式语言提供了一种抽象的计算视图，可以优雅地支持软件工程活动，并且可以进行形式验证。然而，此类语言不支持对计算资源的直接控制，而这正是操作系统、互联网和嵌入式系统等领域所需要的。该项目旨在通过编程结构、语义模型、编译和分析工具来增强此类语言，以控制计算资源，特别是空间使用。尽管该研究重点关注函数式语言，但它解决了 Java 等其他现代编程语言（包括自动空间管理）中常见的问题。所有这些语言都受到不可预测的空间行为的影响，这导致程序员在定位可疑的空间泄漏和优化空间使用上浪费大量资源。 此外，许多方法（例如基于类型的内存线程封装）大多与语言无关，因此普遍适用。这种语言支持的封装的两个可能最令人兴奋的应用是保证互联网上移动代码的安全和并行程序的优化。

Higher-order, typed, functional languages provide an abstract view of computation that supports software engineering activities elegantly, and that is amenable to formal verification. Such languages do not, however, support direct control over computational resources as is needed in domains such as operating systems, the Internet, and embedded systems. This project aims at augmenting such languages with programming constructs, semantic models, compiling and analysis tools for controlling computational resources, particularly space usage. Despite its focus on functional languages, the research addresses a problem common to other modern programming languages like Java that include automatic space management. All such languages suffer from unpredictable space behavior, which causes programmers to waste considerable resources on locating suspected space leaks and optimizing space usage. Furthermore, many of the methods, like the type-based encapsulation of memory threads, are mostly language- independent, and hence universally applicable. Two of the potentially most exciting applications of this language- supported encapsulation are the guaranteeing of safety for mobile code on the Internet and the optimization of parallel programs.