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.