{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T20:24:00Z","timestamp":1764361440755,"version":"3.46.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031997501"},{"type":"electronic","value":"9783031997518"}],"license":[{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-99751-8_13","type":"book-chapter","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T01:21:27Z","timestamp":1759281687000},"page":"302-328","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Custom Representations of\u00a0Inductive Families"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0198-2750","authenticated-orcid":false,"given":"Constantine","family":"Theocharis","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9734-367X","authenticated-orcid":false,"given":"Edwin","family":"Brady","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,1]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-540-27836-8_8","volume-title":"Automata, Languages and Programming","author":"M Abbott","year":"2004","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Representing nested inductive types using W-types. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 59\u201371. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27836-8_8"},{"key":"13_CR2","unstructured":"Abel, A.: Normalization by evaluation: Dependent types and impredicativity. Habilitation thesis, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen. https:\/\/www2.tcs.ifi.lmu.de\/~abel\/talkHabil2013.pdf"},{"key":"13_CR3","unstructured":"Adamek, J., Rosicky, J., Vitale, E.M.: Cambridge tracts in mathematics: algebraic theories: a categorical introduction to general algebra series number 184. Cambridge University Press, Cambridge, England (2010). https:\/\/www.cambridge.org\/academic\/subjects\/mathematics\/logic-categories-and-sets\/algebraic-theories-categorical-introduction-general-algebra?format=HB&isbn=9780521119221"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Allais, G.: Builtin types viewed as inductive families. In: Programming Languages and Systems, pp. 113\u2013139. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_5","DOI":"10.1007\/978-3-031-30044-8_5"},{"key":"13_CR5","unstructured":"Allais, G.: Seamless, correct, and generic programming over serialised data. arXiv (2023). http:\/\/arxiv.org\/abs\/2310.13441"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Allais, G., Brady, E., Corbyn, N., Kammar, O., Yallop, J.: Frex: dependently-typed algebraic simplification. arXiv (2023). https:\/\/doi.org\/10.48550\/ARXIV.2306.15375","DOI":"10.48550\/ARXIV.2306.15375"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 18\u201329. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2837614.2837638","DOI":"10.1145\/2837614.2837638"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Atkey, R.: Syntax and semantics of quantitative type theory. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, pp. 56\u201365. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3209108.3209189","DOI":"10.1145\/3209108.3209189"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Atkey, R., Johann, P., Ghani, N.: When is a type refinement an inductive type? In: Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, pp. 72\u201387. Springer, Heidelberg (2011). https:\/\/bentnib.org\/inductive-refinement.pdf","DOI":"10.1007\/978-3-642-19805-2_6"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Baudon, T., Radanne, G., Gonnord, L.: Bit-stealing made legal: compilation for custom memory representations of algebraic data types. Proc. ACM Program. Lang. 7(ICFP), 813\u2013846 (2023). https:\/\/doi.org\/10.1145\/3607858","DOI":"10.1145\/3607858"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Boulier, S., P\u00e9drot, P.M., Tabareau, N.: The next 700 syntactical models of type theory. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 182\u2013194. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3018610.3018620","DOI":"10.1145\/3018610.3018620"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-24849-1_8","volume-title":"Types for Proofs and Programs","author":"E Brady","year":"2004","unstructured":"Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 115\u2013129. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24849-1_8"},{"key":"13_CR13","unstructured":"Castellan, S., Clairambault, P., Dybjer, P.: Categories with families: unityped, simply typed, and dependently typed. arXiv (2019). http:\/\/arxiv.org\/abs\/1904.00827"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Cockx, J., Devriese, D.: Proof-relevant unification: dependent pattern matching with only the axioms of your type theory. J. Funct. Prog. 28(e12), e12 (2018). https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/E54D56DC3F5D5361CCDECA824030C38E\/S095679681800014Xa.pdf\/div-class-title-proof-relevant-unification-dependent-pattern-matching-with-only-the-axioms-of-your-type-theory-div.pdf","DOI":"10.1017\/S095679681800014X"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Dagand, P.E., McBride, C.: A categorical treatment of ornaments. In: 2013 28th Annual ACM\/IEEE Symposium on Logic in Computer Science. IEEE (2013). https:\/\/doi.org\/10.5555\/2591370.2591396","DOI":"10.5555\/2591370.2591396"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Diehl, L., Firsov, D., Stump, A.: Generic zero-cost reuse for dependent types. Proc. ACM Program. Lang. 2(ICFP), 1\u201330 (2018). https:\/\/doi.org\/10.1145\/3236799","DOI":"10.1145\/3236799"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Goguen, H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Algebra, Meaning, and Computation. Lecture Notes in Computer Science, pp. 521\u2013540. Springer, Heidelberg (2006). https:\/\/research.google.com\/pubs\/archive\/99.pdf","DOI":"10.1007\/11780274_27"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. In: Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science. ACM, New York (2020). https:\/\/doi.org\/10.1145\/3373718.3394736","DOI":"10.1145\/3373718.3394736"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, A.: Staged compilation with two-level type theory. Proc. ACM Program. Lang. 6(ICFP), 540\u2013569 (2022). https:\/\/dl.acm.org\/doi\/10.1145\/3547641","DOI":"10.1145\/3547641"},{"key":"13_CR20","unstructured":"Kov\u00e1cs, A.: Type-theoretic signatures for algebraic theories and inductive types. Ph.D. thesis, E\u00f6tv\u00f6s Lor\u00e1nd University (2023). https:\/\/andraskovacs.github.io\/pdfs\/phdthesis_compact.pdf"},{"key":"13_CR21","unstructured":"Martin-L\u00f6f, P.: Intuitionistic type theory 1, 1\u201391 (1984). https:\/\/intuitionistic.wordpress.com\/wp-content\/uploads\/2010\/07\/martin-lof-tt.pdf"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"McBride, C., Goguen, H., McKinna, J.: A few constructions on constructors. In: Lecture Notes in Computer Science, pp. 186\u2013200. Springer, Heidelberg (2006). http:\/\/www.e-pig.org\/downloads\/concon.pdf","DOI":"10.1007\/11617990_12"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Programming 14(1), 69\u2013111 (2004). https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/F8A44CAC27CCA178AF69DD84BC585A2D\/S0956796803004829a.pdf\/div-class-title-the-view-from-the-left-div.pdf","DOI":"10.1017\/S0956796803004829"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-030-72019-3_17","volume-title":"Programming Languages and Systems","author":"B Moon","year":"2021","unstructured":"Moon, B., Eades III, H., Orchard, D.: Graded modal dependent type theory. In: ESOP 2021. LNCS, vol. 12648, pp. 462\u2013490. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_17"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Views: a way for pattern matching to cohabit with data abstraction. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1987, pp. 307\u2013313. Association for Computing Machinery, New York (1987). https:\/\/doi.org\/10.1145\/41625.41653","DOI":"10.1145\/41625.41653"},{"key":"13_CR26","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Deforestation: transforming programs to eliminate trees. Theor. Comput. Sci. 73(2), 231\u2013248 (1990). https:\/\/www.sciencedirect.com\/science\/article\/pii\/030439759090147A","DOI":"10.1016\/0304-3975(90)90147-A"},{"key":"13_CR27","unstructured":"The Agda Wiki. https:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php. Accessed 3 May 2024"},{"key":"13_CR28","unstructured":"The GNU MP Bignum Library. https:\/\/gmplib.org\/. Accessed 8 Dec 2024"},{"key":"13_CR29","unstructured":"Idris: A Language for Type-Driven Development. https:\/\/www.idris-lang.org\/. Accessed 3 May 2024"},{"key":"13_CR30","unstructured":"Lean: Programming Language and Theorem Prover. https:\/\/lean-lang.org\/. Accessed 3 May 2024"},{"key":"13_CR31","unstructured":"Welcome to a World of Rocq. https:\/\/rocq-prover.org\/. Accessed 16 Apr 2025"},{"key":"13_CR32","unstructured":"agda2hs Documentation \u2014 agda2hs documentation. https:\/\/agda.github.io\/agda2hs\/. Accessed 19 Feb 2025"},{"key":"13_CR33","unstructured":"Should Agda optimise away the erasure from Vec to List? Issue #7701. https:\/\/github.com\/idris-lang\/Idris2\/pull\/3486. Accessed 19 Feb 2025"},{"key":"13_CR34","unstructured":"Program extraction \u2014 Coq 8.13.2 documentation. https:\/\/coq.inria.fr\/doc\/v8.13\/refman\/addendum\/extraction.html. Accessed 19 Feb 2025"},{"key":"13_CR35","unstructured":"Pragmas \u2014 Idris2 0.0 documentation. https:\/\/idris2.readthedocs.io\/en\/latest\/reference\/pragmas.html#transform. Accessed 19 Feb 2025"},{"key":"13_CR36","unstructured":"Make \u2018CONS\u2019, \u2018NIL\u2019, \u2018JUST\u2019 and \u2018NOTHING\u2019 constructors have uniform names by Z-snails. Pull Request #3486. https:\/\/github.com\/idris-lang\/Idris2\/pull\/3486. Accessed 19 Feb 2025"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99751-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,28]],"date-time":"2025-11-28T20:22:17Z","timestamp":1764361337000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99751-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,1]]},"ISBN":["9783031997501","9783031997518"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99751-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,10,1]]},"assertion":[{"value":"1 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TFP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Trends in Functional Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 January 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfp2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/trendsfp.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}