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实用的依赖性功能性编程语言类型系统是一种具有成本效益的轻量级程序验证形式，为程序员提供了一种可机械检查的属性的可访问方式。但是，虽然有用，但实践中使用的类型系统验证了相对较弱的安全性能；他们远远没有计划正确性。这种不表达的部分是由设计 - 完整的验证昂贵，不完全可自动，并且经常没有根据。然而，在许多情况下，指定丰富的程序属性的能力将是有用的。在编程语言的研究人员中，最近有论点认为，来自依赖类型理论的技术在简单类型安全和全面验证之间提供了一系列可能性，该项目的目的是推动实用依赖性的功能编程语言的设计。特别是，研究重点是两种方法： *使用效果型系统来设计完全相关的语言来确保合理性。 *使用全球和本地类型推理的结合，以便可以简单地完成具有依赖类型的编程。对这些方法的评估是通过设计依赖性原型的语言的设计。除上述贡献外，该项目还有助于研究生和本科生的教育。