View Full Document

8 views

Unformatted text preview:

Submitted to POPL 08 An Extensible Theory of Indexed Types Daniel R Licata Robert Harper Carnegie Mellon University drl rwh cs cmu edu Abstract Indexed families of types are a way of associating run time data with compile time abstractions that can be used to reason about them We propose an extensible theory of indexed types in which programmers can define the index data appropriate to their programs and use them to track properties of run time code The essential ingredients in our proposal are 1 a logical framework which is used to define index data constraints and proofs and 2 computation with indices both at the static and dynamic levels of the programming language Computation with indices supports a variety of mechanisms necessary for programming with extensible indexed types including the definition and implementation of indexed types meta theoretic reasoning about indices proofproducing run time checks computed index expressions and runtime actions of index constraints Programmer defined index propositions and their proofs can be represented naturally in a logical framework such as LF where variable binding is used to model the consequence relation of the logic Consequently the central technical challenge in our design is that computing with indices requires computing with the higherorder terms of a logical framework The technical contributions of this paper are a novel method for computing with the higher order data of a simple logical framework and the integration of such computation into the static and dynamic levels of a programming language Further we present examples showing how this computation supports indexed programming 1 Introduction One way to enrich the expressiveness of a type system is to provide the programmer with a rich language of data that can be used at compile time to state and verify properties of run time code Compile time data can be associated with run time values using an indexed family of types whose indices vary with the classified



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view paper and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view paper and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?