A Practical Dependently-Typed Functional Programming Language

实用的依赖类型函数式编程语言静态类型系统是轻量级程序验证的一种经济有效的形式，为程序员提供了一种易于处理的方式来表达可以机械地检查的属性。然而，尽管有帮助，实践中使用的类型系统验证了相对较弱的安全特性；它们远远达不到程序正确性的要求。这种缺乏表现力部分是由设计造成的——完整的验证是昂贵的，不是完全自动化的，而且通常是没有保证的。尽管如此，在许多情况下，指定富程序属性的能力将是有用的。在编程语言研究人员中，最近有一种观点认为，依赖类型理论的技术在简单类型安全和完全验证之间提供了一系列可能性。这个项目的目标是推进实用的依赖类型函数式编程语言的设计。特别地，研究集中在两种方法上：*设计一种完全依赖类型的语言，使用效果类型系统来确保稳健性。*使用全局和局部类型推断的结合，使得使用依赖类型的编程可以简洁地完成。这些方法的评估是通过设计一个原型依赖类型的语言。除了上述贡献外，该项目还有助于研究生和本科生的教育。

NSF 0702545Weirich, StephanieU of PennsylvaniaA Practical Dependently-typed Functional Programming LanguageStatic type systems are a cost-effective form of lightweight program verification, providing a tractable way for programmers to express properties that can be mechanically checked. However, while helpful,type systems used in practice verify relatively weak safety properties; they fall far short of program correctness. This inexpressiveness is partly by design---full verification is expensive, not fully automatable, and often unwarranted. Nevertheless, there are many situations where the ability to specify rich program properties would be useful. Among programming-language researchers, there is recent argument that techniques from dependent type theory provide a spectrum of possibilities between simple type safety and full verificationThe goal of this project is to advance the design of practical dependently-typed functional programming languages. In particular, the research focuses on two approaches: * To design a fully dependently-typed language, using an effect-type system to ensure soundness. * To employ a combination of global and local type inference so that programming with dependent types may be done concisely.The evaluation of these approaches is through the design of a prototype dependently-typed language. As well as the contributions listed above, this project aids the education of both graduate and undergraduate students.