TACL Seminar Fall '04
Fall '04 Schedule
|Aug 12||xinming Ou||Dynamic Typing with Dependent Types||Abstract|
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 adependent type checker verifies them at compile time. Other fragments are marked "simple", in which case they may be annotation-free and dependent constraints are verified at run time.