TACL Seminar Fall '04

From CSWiki
Revision as of 04:38, 27 August 2006 by Ddantas (talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

TACL Seminar

Fall '04 Schedule

Date Speaker Title Links
Aug 12 xinming Ou Dynamic Typing with Dependent Types Abstract


Xinming Ou

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.

TACL Seminar