SHF:Large:Collaborative Research:TRELLYS: Community-Based Design and Implementation of a Dependently Typed Programming Language

SHF：大型：协作研究：TRELLYS：基于社区的依赖类型编程语言的设计和实现

• 批准号: 0910786
• 负责人: Stephanie Weirich
• 金额: $ 71万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-09-01 至 2014-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0910786&HistoricalAwards=false
• 关键词: SHF; Large; Collaborative; Research; TRELLYS

The cost-effective construction of functionally correct software systems remains an unmet challenge for Computer Science. Although industrial best practices for software construction (such as testing, code reviews, automatic bug finding) have low cost, they cannot provide strong guarantees about correctness. Classical verification methods, on the other hand, are not cost-effective. Recently, the research community has been exploring the idea of dependent types, which extend the expressive power of programming languages to support verification. These rich types allow the programmer to express non-trivial invariant properties of her data and code as a part of her program. That way, verification is incremental, localized and at source-language level.This multi-institution collaborative project is for the design and implementation of a programming language with dependent types, called Trellys. Technically, Trellys is call-by-value functional programming language with full-spectrum dependency. Overall, the project combines numerous fragmented research results into a coherent language design, by building a robust open-source implementation. The design draws on diverse solutions to the technical problems that arise from extending traditional programming languages accommodate dependent types: type and effect inference, language interoperability, compilation, and concurrency.

功能正确的软件系统的成本效益构建仍然是计算机科学尚未解决的挑战。尽管软件构建的工业最佳实践（例如测试、代码审查、自动错误查找）成本较低，但它们无法提供正确性的有力保证。另一方面，经典验证方法并不具有成本效益。 最近，研究社区一直在探索依赖类型的想法，它扩展了编程语言的表达能力以支持验证。这些丰富的类型允许程序员将数据和代码的重要不变属性表达为程序的一部分。这样，验证是增量的、本地化的和源语言级别的。这个多机构协作项目旨在设计和实现具有依赖类型的编程语言，称为 Trellys。从技术上讲，Trellys 是一种具有全谱依赖性的按值调用函数式编程语言。总体而言，该项目通过构建强大的开源实现，将众多零碎的研究成果结合到一个连贯的语言设计中。该设计借鉴了多种解决方案来解决因扩展传统编程语言以适应依赖类型而产生的技术问题：类型和效果推断、语言互操作性、编译和并发性。