A Practical Dependently-Typed Functional Programming Language

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

NSF 0702545 Weirich, Stephanie U of Pennsylvania A Practical Dependently-typed Functional Programming Language Static 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 verification The 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.