{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T13:44:08Z","timestamp":1770385448328,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540221647","type":"print"},{"value":"9783540248491","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_8","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:34:24Z","timestamp":1281299664000},"page":"115-129","source":"Crossref","is-referenced-by-count":42,"title":["Inductive Families Need Not Store Their Indices"],"prefix":"10.1007","author":[{"given":"Edwin","family":"Brady","sequence":"first","affiliation":[]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Hofmann, M., Streicher, T.: Categorical reconstruction of a reduction free normalization proof (1996)","DOI":"10.1007\/3-540-60164-3_27"},{"key":"8_CR2","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/3-540-15975-4_48","volume-title":"Functional Programming Languages and Computer Architecture","author":"L. Augustsson","year":"1985","unstructured":"Augustsson, L.: Compiling pattern matching. In: Jouannaud, J.-P. (ed.) Functional Programming Languages and Computer Architecture, September 1985, pp. 368\u2013381. Springer, Heidelberg (1985)"},{"key":"8_CR3","unstructured":"Augustsson, L., Carlsson, M.: An exercise in dependent types: A well-typed interpreter (1999), http:\/\/www.cs.chalmers.se\/~augustss\/cayenne\/"},{"issue":"5","key":"8_CR4","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1093\/logcom\/6.5.663","volume":"6","author":"S. Berardi","year":"1996","unstructured":"Berardi, S.: Pruning simply typed lambda terms. Journal of Logic and Computation\u00a06(5), 663\u2013681 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/LICS.1991.151645","volume-title":"Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science","author":"U. Berger","year":"1991","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed \u03bb-calculus. In: Vemuri, R. (ed.) Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 203\u2013211. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bove, A., Capretta, V.: Modelling general recursion in type theory (September 2002)","DOI":"10.1007\/3-540-39185-1_3"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/3-540-44557-9_6","volume-title":"Types for Proofs and Programs","author":"P. Callaghan","year":"2000","unstructured":"Callaghan, P., Luo, Z.: Implementation techniques for inductive types in plastic. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 94\u2013113. Springer, Heidelberg (2000)"},{"key":"8_CR8","unstructured":"Coq Development Team. The Coq proof assistant \u2014 reference manual (2001)"},{"key":"8_CR9","unstructured":"Andr\u00e9 Lu\u00b4\u0131s de Medeiros Santos. Compilation By Transformatio. In: Non-Strict Functional Languages. PhD thesis, University of Glasgow (1995)"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal Aspects Of Computing\u00a06, 440\u2013465 (1994)","journal-title":"Formal Aspects Of Computing"},{"issue":"1","key":"8_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0304-3975(90)90108-T","volume":"89","author":"R. Harper","year":"1991","unstructured":"Harper, R., Pollack, R.: Type checking with universes. Theoretical Computer Science\u00a089(1), 107\u2013136 (1991)","journal-title":"Theoretical Computer Science"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Johnsson, T.: Efficient compilation of lazy evaluation (1984)","DOI":"10.1145\/502874.502880"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Luo, Z.: Computation and Reasoning \u2013 A Type Theory for Computer Science. International Series of Monographs on Computer Science. OUP (1994)","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"8_CR15","unstructured":"Luo, Z., Pollack, R.: Lego proof development system: User\u2019s manual. Technical report, LFCS, University of Edinburgh (1992)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-45842-5_12","volume-title":"Types for Proofs and Programs","author":"N. Magaud","year":"2002","unstructured":"Magaud, N., Bertot, Y.: Changing data structures in type theory: A study of natural numbers. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 181\u2013196. Springer, Heidelberg (2002)"},{"key":"8_CR17","unstructured":"Magnusson, L.: The implementation of ALF \u2013 A Proof Editor based on Martin- L\u00f6f\u2019s Monomorphic Type Theory with Explicit Substitutions. PhD thesis, Chalmers University of Technology, G\u00f6teborg (1994)"},{"key":"8_CR18","unstructured":"McBride, C.: Dependently Typed Functional Programs and their proofs. PhD thesis, University of Edinburgh (May 2000)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming\u00a014(1) (2004)","DOI":"10.1017\/S0956796803004829"},{"key":"8_CR20","unstructured":"McBride, F.: Computer Aided Manipulation of Symbols. PhD thesis, Queen\u2019s University of Belfast (1970)"},{"key":"8_CR21","unstructured":"Paulin-Mohring, C.: Extraction de programmes dans le Calcul des Constructions. PhD thesis, Paris 7 (1989)"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0167-6423(97)00029-4","volume":"32","author":"S.L.P. Jones","year":"1998","unstructured":"Jones, S.L.P., Santos, A.L.M.: A transformation-based optimiser for Haskell. Science of Computer Programming\u00a032, 3\u201347 (1998)","journal-title":"Science of Computer Programming"},{"key":"8_CR23","unstructured":"Pollack, R.: Implicit syntax. Technical report, LFCS, University of Edinburgh (1992)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Sansom, P.M., Jones, S.L.P.: Time and space profiling for non-strict, higher order functional languages (1995)","DOI":"10.1145\/199448.199531"},{"key":"8_CR25","unstructured":"Xi, H.: Dependent Types in Practical Programming. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University (December 1998)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Xi, H.: Dead code elimination through dependent types (1999)","DOI":"10.1007\/3-540-49201-1_16"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types (1998)","DOI":"10.1145\/277650.277732"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,29]],"date-time":"2024-03-29T05:59:00Z","timestamp":1711691940000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}