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

如何经济高效地构建功能正确的软件系统仍然是计算机科学面临的一个挑战。尽管软件构建的工业最佳实践（例如测试、代码审查、自动bug发现）成本较低，但它们不能提供对正确性的强有力保证。另一方面，经典的验证方法并不具有成本效益。最近，研究团体一直在探索依赖类型的概念，它扩展了编程语言的表达能力，以支持验证。这些丰富的类型允许程序员将数据和代码的重要不变属性表示为程序的一部分。这样，验证是增量的、本地化的和源语言级别的。这个多机构合作项目是为了设计和实现一种具有依赖类型的编程语言，称为Trellys。从技术上讲，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.