A Practical Dependently-Typed Functional Programming Language

一种实用的依赖类型函数编程语言

基本信息

批准号：
0702545
负责人：
Stephanie Weirich
金额：
$ 20万
依托单位：
University of Pennsylvania
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2007
资助国家：
美国
起止时间：
2007-05-15 至 2010-04-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=0702545&HistoricalAwards=false
关键词：
Practical Dependently Typed Functional Programming

项目摘要

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.

NSF 0702545Weirich，StephanieU，宾夕法尼亚州实用的依赖类型函数编程语言静态类型系统是一种经济高效的轻量级程序验证形式，为程序员提供了一种易于处理的方式来表达可以机械检查的属性。然而，虽然有用，但实践中使用的类型系统验证了相对较弱的安全属性；它们远远达不到程序的正确性。这种缺乏表现力的部分原因是设计造成的——全面验证成本高昂，不能完全自动化，而且通常是没有根据的。然而，在许多情况下，指定丰富的程序属性的能力会很有用。在编程语言研究人员中，最近有一种观点认为，依赖类型理论的技术提供了简单类型安全和完全验证之间的一系列可能性。该项目的目标是推进实用的依赖类型函数编程语言的设计。具体来说，该研究侧重于两种方法： * 设计完全依赖类型的语言，使用效果类型系统来确保健全性。 * 采用全局和局部类型推断的组合，以便可以简洁地完成依赖类型的编程。这些方法的评估是通过原型依赖类型语言的设计来进行的。除了上面列出的贡献外，该项目还帮助研究生和本科生的教育。