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

对于计算机科学来说，经济有效地构建功能正确的软件系统仍然是一个尚未满足的挑战。尽管软件构建的行业最佳实践(如测试、代码审查、自动错误查找)的成本很低，但它们不能为正确性提供强有力的保证。另一方面，经典的验证方法并不划算。最近，研究界一直在探索依赖类型的思想，它扩展了编程语言的表达能力，以支持验证。这些丰富的类型允许程序员将她的数据和代码的重要不变属性表示为她的程序的一部分。这样，验证是增量的、本地化的和源语言级别的。这个多机构合作的项目是为了设计和实现一种具有依赖类型的编程语言，称为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.