Dynamic typing with dependent types

Xinming Ou, Gang Tan, Yitzhak Mandelbaum, David Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

50 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationExploring New Frontiers of Theoretical Informatics - IFIP 18th World Computer Congress TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004
PublisherSpringer New York LLC
Pages437-450
Number of pages14
ISBN (Print)1402081405, 9781402081408
DOIs
StatePublished - 2004
EventIFIP 18th World Computer Congress, TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004 - Toulouse, France
Duration: Aug 22 2004Aug 27 2004

Publication series

NameIFIP Advances in Information and Communication Technology
Volume155
ISSN (Print)1868-4238

Other

OtherIFIP 18th World Computer Congress, TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004
CountryFrance
CityToulouse
Period8/22/048/27/04

All Science Journal Classification (ASJC) codes

  • Information Systems
  • Computer Networks and Communications
  • Information Systems and Management

Fingerprint Dive into the research topics of 'Dynamic typing with dependent types'. Together they form a unique fingerprint.

  • Cite this

    Ou, X., Tan, G., Mandelbaum, Y., & Walker, D. (2004). Dynamic typing with dependent types. In Exploring New Frontiers of Theoretical Informatics - IFIP 18th World Computer Congress TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004 (pp. 437-450). (IFIP Advances in Information and Communication Technology; Vol. 155). Springer New York LLC. https://doi.org/10.1007/1-4020-8141-3_34