@inbook{63ff7863e33448d090d6d2f99b8cfe96,
title = "Inductive Families Need Not Store Their Indices",
abstract = "We consider the problem of efficient representation of dependently typed data. In particular, we consider a language TT based on Dybjer{\textquoteright}s notion of inductive families [10] and reanalyse their general form with a view to optimising the storage associated with their use. We introduce an execution language, ExTT, which allows the commenting out of computationally irrelevant subterms and show how to use properties of elimination rules to elide constructor arguments and tags in ExTT. We further show how some types can be collapsed entirely at run-time. Several examples are given, including a representation of the simply typed λ-calculus for which our analysis yields an 80% reduction in run-time storage requirements.",
author = "Edwin Brady and Conor McBride and James Mckinna",
year = "2004",
doi = "10.1007/978-3-540-24849-1_8",
language = "English",
isbn = "9783540221647",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "115--129",
booktitle = "Types for Proofs and Programs. TYPES 2003",
note = "3rd Annual Workshop of the Types Working Group 2003, TYPES 2003 ; Conference date: 30-04-2003 Through 04-05-2003",
}