SHF: Small: Typed Self-Application

SHF：小型：类型自应用

• 批准号: 1219240
• 负责人: Jens Palsberg
• 金额: $ 49.36万
• 依托单位: University of California-Los Angeles
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-09-01 至 2018-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1219240&HistoricalAwards=false
• 关键词: SHF; Small; Typed; Self; Application

Static type checking has brought us more reliable software. Types make programs more readable, prevent entire classes of mistakes, and help compilers optimize data layout and data access. Types also make it easier to use libraries and to design interfaces, and they make it harder to misuse data and write bad programs. An entirely different trend is as old as programming: self-application. In particular, self-application is popular in the form of implementing a language in itself. When the trends of types and self-application meet, a fundamental challenge for type systems arises. For example, what is the type of an interpreter that can interpret a representation of itself? And what is the type of a compiler that can compile a representation of itself? The goal of the project is to enable the next generation of typed, self-applicable interpreters, compilers, and partial evaluators. This next generation will guarantee that the output represents a typed program, and that the type of the output program is related to the type of the input program. The result will be self-applicable meta-programs that are more reliable and have all the benefits of static type checking.Many popular languages have a self-interpreter, that is, an interpreter for the language written in itself; examples include Standard ML, Haskell, Scheme, JavaScript, Python, and Ruby. Similarly, many languages have self-compilers, that is, a compiler for the language written in itself. Also, some languages have a virtual machine written in itself, including Java and Self. The project will bring static type checking to self-applicable interpreters, compilers, and partial evaluators, and take such meta-programs to a higher level of reliability by ensuring that the output programs type check and therefore cannot contain entire classes of mistakes. The investigator will teach the results to students as part of existing undergraduate and graduate courses.

静态类型检查给我们带来了更可靠的软件。 类型使程序更具可读性，防止整类错误，并帮助编译器优化数据布局和数据访问。 类型也使使用库和设计接口变得更容易，并且使误用数据和编写糟糕的程序变得更困难。 另一种完全不同的趋势与编程一样古老：自我应用。 特别是，自我应用以实现语言本身的形式流行。 当类型和自应用的趋势相遇时，类型系统的一个基本挑战就出现了。 例如，什么类型的解释器可以解释自己的表示？ 什么类型的编译器可以编译自身的表示？ 该项目的目标是实现下一代类型化的、自适用的解释器、编译器和部分求值器。 下一代将保证输出表示类型化程序，并且输出程序的类型与输入程序的类型相关。 许多流行的语言都有一个自解释器，也就是说，一个解释器可以解释用自己编写的语言，例如标准ML、Haskell、Scheme、JavaScript、Python和Ruby。 类似地，许多语言都有自编译器，也就是说，一个编译器为自己编写的语言。 此外，一些语言本身也有一个虚拟机，包括Java和Self。 该项目将把静态类型检查带到自适用的解释器、编译器和部分求值器中，并通过确保输出程序的类型检查，从而不会包含整个错误类，将此类元程序提高到更高的可靠性水平。 研究人员将把结果作为现有本科和研究生课程的一部分教授给学生。