SHF: Small: Principled Compiling and Linking for Multi-Language Software

SHF：小型：多语言软件的原则性编译和链接

• 批准号: 1816837
• 负责人: Amal Ahmed
• 金额: $ 44.98万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-10-01 至 2022-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1816837&HistoricalAwards=false
• 关键词: SHF; Small; Principled; Compiling; Linking

When building large software systems, programmers should be able to use the best language for each part of the system. But when a component written in one language becomes part of a multi-language system, it may interoperate with components that have features that don't exist in the original language. This affects programmers when they refactor code (i.e., make changes that should result in equivalent behavior). Since programs interact after compilation to a common target, programmers have to understand details of linking and target-level interaction when reasoning about correctly refactoring source components. Unfortunately, there are no software toolchains available today that support single-language reasoning when components are used in a multi-language system. This project will develop principled software toolchains for building multi-language software. The project's novelties include (1) designing language extensions that allow programmers to specify how they wish to interoperate (or link) with conceptual features absent from their language through a mechanism called linking types, and (2) developing compilers that formally guarantee that any reasoning the programmer does at source level is justified after compilation to the target. The project has the potential for tremendous impact on the software development landscape as it will allow programmers to use a language close to their problem domain and provide them with software toolchains that make it easy to compose components written in different languages into a multi-language software system.The project will evaluate the idea of linking types by extending ML with linking types for interaction with Rust, a language with first-class control, and a normalizing language, and developing type preserving compilers to a common typed LLVM-like target language. The project will design a rich dependently typed LLVM-like target language that can encapsulate effects from different source languages to support fully abstract compilation from these languages. The project will also investigate reporting of cross-language type errors to aid programmers when composing components written in different languages.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

在构建大型软件系统时，程序员应该能够为系统的每个部分使用最好的语言。 但是，当一个用一种语言编写的组件成为多语言系统的一部分时，它可能会与具有原始语言中不存在的功能的组件进行互操作。 这会影响程序员重构代码（即，做出应导致等效行为的更改）。 由于程序在编译到公共目标后进行交互，因此程序员在推理正确重构源组件时必须了解链接和目标级交互的细节。 不幸的是，当组件用于多语言系统时，目前还没有软件工具链支持单语言推理。 该项目将开发用于构建多语言软件的原则性软件工具链。 该项目的新颖之处包括：（1）设计语言扩展，允许程序员通过一种称为链接类型的机制指定他们希望如何与他们的语言中缺少的概念特性进行互操作（或链接），以及（2）开发编译器，正式保证程序员在源代码级别进行的任何推理在编译到目标之后都是合理的。 该项目有可能对软件开发领域产生巨大的影响，因为它将允许程序员使用接近其问题领域的语言，并为他们提供软件工具链，使他们可以轻松地将用不同语言编写的组件组合到多语言软件系统中。该项目将评估通过使用链接类型扩展ML以与Rust交互的链接类型的想法，一种具有一流控制的语言和一种规范化语言，并将类型保持编译器开发为一种公共类型化的LLVM目标语言。 该项目将设计一种丰富的依赖类型的LLVM目标语言，可以封装来自不同源语言的效果，以支持这些语言的完全抽象编译。 该项目还将调查跨语言类型错误的报告，以帮助程序员在编写不同语言的组件时。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。

项目成果

Under Control: Compositionally Correct Closure Conversion with Mutable State

受控：具有可变状态的组合正确的闭包转换

• DOI: 10.1145/3354166.3354181
• 发表时间: 2019
• 期刊: Principles and Practice of Programming Languages 2019 (PPDP ’19
• 作者: Mates, Phillip;Perconti, Jamie;Ahmed, Amal
• 通讯作者: Ahmed, Amal

The next 700 compiler correctness theorems (functional pearl)

• DOI: 10.1145/3341689
• 发表时间: 2019-07
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Daniel Patterson;Amal J. Ahmed

Gradual type theory

渐进式理论

• DOI: 10.1017/s0956796821000125
• 发表时间: 2021
• 期刊: Journal of Functional Programming
• 影响因子: 1.1
• 作者: NEW, MAX S.;LICATA, DANIEL R.;AHMED, AMAL
• 通讯作者: AHMED, AMAL

Graduality and parametricity: together again for the first time

渐进性和参数化：首次再次结合在一起

• DOI: 10.1145/3371114
• 发表时间: 2020
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: New, Max S.;Jamner, Dustin;Ahmed, Amal
• 通讯作者: Ahmed, Amal

Semantic soundness for language interoperability

语言互操作性的语义健全性

• DOI: 10.1145/3519939.3523703
• 发表时间: 2022
• 期刊: Proceed- ings of the 43rd ACM SIGPLAN International Conference on Program- ming Language Design and Implementation (PLDI ’22
• 作者: Patterson, Daniel;Mushtak, Noble;Wagner, Andrew;Ahmed, Amal
• 通讯作者: Ahmed, Amal