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.