{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:09Z","timestamp":1776891429928,"version":"3.51.2"},"reference-count":43,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,5,20]],"date-time":"2015-05-20T00:00:00Z","timestamp":1432080000000},"content-version":"unspecified","delay-in-days":139,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.<\/jats:p>","DOI":"10.1017\/s095679681500009x","type":"journal-article","created":{"date-parts":[[2015,5,20]],"date-time":"2015-05-20T03:22:51Z","timestamp":1432092171000},"source":"Crossref","is-referenced-by-count":37,"title":["Indexed containers"],"prefix":"10.46298","volume":"25","author":[{"given":"THORSTEN","family":"ALTENKIRCH","sequence":"first","affiliation":[]},{"given":"NEIL","family":"GHANI","sequence":"additional","affiliation":[]},{"given":"PETER","family":"HANCOCK","sequence":"additional","affiliation":[]},{"given":"CONOR","family":"MCBRIDE","sequence":"additional","affiliation":[]},{"given":"PETER","family":"MORRIS","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2015,5,20]]},"reference":[{"key":"S095679681500009X_ref31","unstructured":"McBride C. (2001) The derivative of a regular type is its type of one-hole contexts. Available online."},{"key":"S095679681500009X_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.07.001"},{"key":"S095679681500009X_ref43","unstructured":"Turner D. A. (1985) Elementary strong functional programming. In 1st International Symposium on Functional Programming Languages in Education. Springer, LNCS 1022, pp. 1\u201313."},{"key":"S095679681500009X_ref41","unstructured":"The Agda Team. (2015) The agda wiki. Available at: http:\/\/wiki.portal.chalmers.se\/agda\/agda.php."},{"key":"S095679681500009X_ref37","doi-asserted-by":"crossref","unstructured":"Nordvall Forsberg F. and Setzer A. (2010) Inductive-inductive definitions. In Proceedings of the 24th International Conference\/19th Annual Conference on Computer Science Logic, pp. 454\u2013468. Citeseer.","DOI":"10.1007\/978-3-642-15205-4_35"},{"key":"S095679681500009X_ref36","unstructured":"Nordvall Forsberg F. (2013) Inductive-inductive definitions. PhD thesis, Swansea University."},{"key":"S095679681500009X_ref34","unstructured":"Morris P. , Altenkirch T. & Ghani N. (2007a) Constructing strictly positive families. In The Australasian Theory Symposium (CATS2007). ACS, pp 111\u2013121."},{"key":"S095679681500009X_ref33","unstructured":"Morris P. & Altenkirch T. (2009) Indexed containers. In 24th IEEE Symposium in Logic in Computer Science (LICS 2009). IEEE, pp 277\u2013285."},{"key":"S095679681500009X_ref32","unstructured":"McBride C. (2010) Ornamental algebras, algebraic ornaments. Available online."},{"key":"S095679681500009X_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"S095679681500009X_ref30","volume-title":"Categories for the Working Mathematician","author":"Ma cLane","year":"1998"},{"key":"S095679681500009X_ref29","doi-asserted-by":"publisher","DOI":"10.2307\/2275015"},{"key":"S095679681500009X_ref27","first-page":"126","volume-title":"Combinatoire \u00e9numerative","author":"Joyal","year":"1987"},{"key":"S095679681500009X_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_68"},{"key":"S095679681500009X_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90025-5"},{"key":"S095679681500009X_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"S095679681500009X_ref20","volume-title":"Types for Proofs and Programs (TYPES 2003)","author":"Gambino","year":"2004"},{"key":"S095679681500009X_ref19","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/jdm096"},{"key":"S095679681500009X_ref15","unstructured":"Danielsson N. A. & Altenkirch T. (2010) Subtyping, declaratively; an exercise in mixed induction and coinduction. In Proceedings of the 9th International Conference on Mathematics of Program Construction (MPC 10). Springer, LNCS 6120, pp 100\u2013118."},{"key":"S095679681500009X_ref42","unstructured":"The Coq Development Team. (2008) The Coq Proof Assistant Reference Manual \u2013 Version 8.1."},{"key":"S095679681500009X_ref14","unstructured":"Cheney J. & Hinze R. (2003) First-class phantom types. Cornell University, Techn. Report."},{"key":"S095679681500009X_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00011-K"},{"key":"S095679681500009X_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_21"},{"key":"S095679681500009X_ref12","volume-title":"Algebra of programming","author":"Bird","year":"1997"},{"key":"S095679681500009X_ref40","unstructured":"The Agda developers. (2015) The agda wiki. on the web."},{"key":"S095679681500009X_ref28","doi-asserted-by":"crossref","unstructured":"Kock J. (2009) Notes on polynomial functors. Manuscript, available online.","DOI":"10.1093\/imrn\/rnq068"},{"key":"S095679681500009X_ref38","doi-asserted-by":"crossref","unstructured":"Petersson K. & Synek D. (1989) A set constructor for inductive sets in Martin-L\u00f6f's type theory. In Proceedings of the 1989 Conference on Category Theory and Computer Science, Manchester, UK: Springer Verlag, Lecture Notes in Computer Science, vol. 389.","DOI":"10.1007\/BFb0018349"},{"key":"S095679681500009X_ref6","doi-asserted-by":"crossref","unstructured":"Altenkirch T. , Ghani N. , McBride C. & Morris P. (2015) Agda sources for indexed containers. Available at: http:\/\/cs.not.ac.uk\/~txa\/ic-code\/.","DOI":"10.1017\/S095679681500009X"},{"key":"S095679681500009X_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"S095679681500009X_ref39","doi-asserted-by":"crossref","unstructured":"Sozeau M. (2007) Subset coercions in Coq. In TYPES 2006, Lecture Notes in Computer Science, vol. 4502. p. 237.","DOI":"10.1007\/978-3-540-74464-1_16"},{"key":"S095679681500009X_ref11","volume-title":"Categories, Types, and Structures","author":"Asperti","year":"1991"},{"key":"S095679681500009X_ref13","first-page":"3","volume-title":"ACM Sigplan Notices","author":"Chapman","year":"2010"},{"key":"S095679681500009X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45504-3_7"},{"key":"S095679681500009X_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00145-4"},{"key":"S095679681500009X_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2005.05.022"},{"key":"S095679681500009X_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"S095679681500009X_ref9","unstructured":"Altenkirch T. , Nordvall Forsberg F. , Morris P. and Setzer A. (2011) A categorical semantics for inductive-inductive definitions. In CALCO 2011: 4th International Conference on Algebra and Coalgebra in Computer Science. Springer, LNCS 6859, pp 70\u201384."},{"key":"S095679681500009X_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13962-8_2"},{"key":"S095679681500009X_ref35","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006462"},{"key":"S095679681500009X_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007278"},{"key":"S095679681500009X_ref24","doi-asserted-by":"crossref","unstructured":"Hancock P. , McBride C. , Ghani N. , Malatesta L. & Altenkirch T. (2013) Small induction recursion. In Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, pp. 156\u2013172.","DOI":"10.1007\/978-3-642-38946-7_13"},{"key":"S095679681500009X_ref8","first-page":"57","volume-title":"Programming Languages meet Program Verification (PLPV2007)","author":"Altenkirch","year":"2007"},{"key":"S095679681500009X_ref1","doi-asserted-by":"crossref","unstructured":"Abbott M. , Altenkirch T. & Ghani N. (2003) Categories of containers. In Proceedings of Foundations of Software Science and Computation Structures. Springer, LNCS 2620, pp. 23\u201338.","DOI":"10.1007\/3-540-36576-1_2"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S095679681500009X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:45Z","timestamp":1776889185000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S095679681500009X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":43,"alternative-id":["S095679681500009X"],"URL":"https:\/\/doi.org\/10.1017\/s095679681500009x","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"article-number":"e5"}}