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是具有全谱依赖的按值调用函数式编程语言。总体而言，该项目通过构建一个强大的开源实现，将众多零散的研究成果结合到一个连贯的语言设计中。该设计借鉴了各种解决方案，以解决扩展传统编程语言所产生的技术问题，以适应依赖类型：类型和效果推理，语言互操作性，编译和并发性。