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.