Dynamic Typing with Dependent Types

11 years 11 months ago
Dynamic Typing with Dependent Types
Dependent type systems are promising tools programmers can use to increase the reliability and security of their programs. Unfortunately, dependently-typed programming languages require programmers to annotate their programs with many typing specifications to help guide the type checker. This paper shows how to make the process of programming with dependent types more palatable by defining a language in which programmers have fine-grained control over the trade-off between the number of dependent typing annotations they must place on programs and the degree of compile-time safety. More specifically, certain program fragments are marked dependent, in which case the programmer annotates them in detail and a dependent type checker verifies them at compile time. Other fragments are marked simple, in which case they may be annotationfree and dependent constraints are verified at run time.
Xinming Ou, Gang Tan, Yitzhak Mandelbaum, David Wa
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where IFIP
Authors Xinming Ou, Gang Tan, Yitzhak Mandelbaum, David Walker
Comments (0)