Dynamic typing with dependent types

Xinming Ou, Gang Tan, Yitzhak Mandelbaum, David Walker

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

47 Citations (Scopus)

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
Volume155
ISBN (Print)1402081405, 9781402081408
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)18684238

Other

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

Fingerprint

Language
Programming
Trade-offs
Safety
Annotation

All Science Journal Classification (ASJC) codes

  • Information Systems and Management

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 (Vol. 155, pp. 437-450). (IFIP Advances in Information and Communication Technology; Vol. 155). Springer New York LLC.
Ou, Xinming ; Tan, Gang ; Mandelbaum, Yitzhak ; Walker, David. / Dynamic typing with dependent types. Exploring New Frontiers of Theoretical Informatics - IFIP 18th World Computer Congress TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004. Vol. 155 Springer New York LLC, 2004. pp. 437-450 (IFIP Advances in Information and Communication Technology).
@inproceedings{ea635e6df986451f98f7f89f2babc984,
title = "Dynamic typing with dependent types",
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.",
author = "Xinming Ou and Gang Tan and Yitzhak Mandelbaum and David Walker",
year = "2004",
language = "English (US)",
isbn = "1402081405",
volume = "155",
series = "IFIP Advances in Information and Communication Technology",
publisher = "Springer New York LLC",
pages = "437--450",
booktitle = "Exploring New Frontiers of Theoretical Informatics - IFIP 18th World Computer Congress TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004",

}

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. vol. 155, IFIP Advances in Information and Communication Technology, vol. 155, Springer New York LLC, pp. 437-450, IFIP 18th World Computer Congress, TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004, Toulouse, France, 8/22/04.

Dynamic typing with dependent types. / Ou, Xinming; Tan, Gang; Mandelbaum, Yitzhak; Walker, David.

Exploring New Frontiers of Theoretical Informatics - IFIP 18th World Computer Congress TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004. Vol. 155 Springer New York LLC, 2004. p. 437-450 (IFIP Advances in Information and Communication Technology; Vol. 155).

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

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

M3 - Conference contribution

AN - SCOPUS:84901048150

SN - 1402081405

SN - 9781402081408

VL - 155

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

ER -

Ou X, Tan G, Mandelbaum Y, Walker D. 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. Vol. 155. Springer New York LLC. 2004. p. 437-450. (IFIP Advances in Information and Communication Technology).