TY - GEN
T1 - Dynamic typing with dependent types
AU - Ou, Xinming
AU - Tan, Gang
AU - Mandelbaum, Yitzhak
AU - Walker, David
PY - 2004
Y1 - 2004
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84901048150&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84901048150&partnerID=8YFLogxK
U2 - 10.1007/1-4020-8141-3_34
DO - 10.1007/1-4020-8141-3_34
M3 - Conference contribution
AN - SCOPUS:84901048150
SN - 1402081405
SN - 9781402081408
T3 - IFIP Advances in Information and Communication Technology
SP - 437
EP - 450
BT - Exploring New Frontiers of Theoretical Informatics - IFIP 18th World Computer Congress TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004
PB - Springer New York LLC
T2 - IFIP 18th World Computer Congress, TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004
Y2 - 22 August 2004 through 27 August 2004
ER -