{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:10Z","timestamp":1753889770675,"version":"3.41.2"},"reference-count":37,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,6,4]],"date-time":"2012-06-04T00:00:00Z","timestamp":1338768000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Dependently typed programming languages allow sophisticated properties of\ndata to be expressed within the type system. Of particular use in dependently\ntyped programming are indexed types that refine data by computationally useful\ninformation. For example, the N-indexed type of vectors refines lists by their\nlengths. Other data types may be refined in similar ways, but programmers must\nproduce purpose-specific refinements on an ad hoc basis, developers must\nanticipate which refinements to include in libraries, and implementations must\noften store redundant information about data and their refinements. In this\npaper we show how to generically derive inductive characterisations of\nrefinements of inductive types, and argue that these characterisations can\nalleviate some of the aforementioned difficulties associated with ad hoc\nrefinements. Our characterisations also ensure that standard techniques for\nprogramming with and reasoning about inductive types are applicable to\nrefinements, and that refinements can themselves be further refined.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:9)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":5,"title":["Refining Inductive Types"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4414-5047","authenticated-orcid":false,"given":"Robert","family":"Atkey","sequence":"first","affiliation":[]},{"given":"Patricia","family":"Johann","sequence":"additional","affiliation":[]},{"given":"Neil","family":"Ghani","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,6,4]]},"reference":[{"issue":"1","key":"10.2168\/LMCS-8(2:9)2012_DBLP:conf\/fossacs\/AbbottAG03","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2005.06.002","volume":"342","author":"M. Abbott, T. Altenkirch, and N. Ghani","year":"2005","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(2:9)2012_amm07","doi-asserted-by":"crossref","unstructured":"T. Altenkirch, C. McBride, and P. Morris. Generic programming with dependent types. In R. Backhouse, J. Gibbons, R. Hinze, and J. Jeuring, editors,Datatype-Generic Programming, volume 4719 ofLecture Notes in Computer Science, pages 209-257. Springer, 2007.","DOI":"10.1007\/978-3-540-76786-2_4"},{"key":"10.2168\/LMCS-8(2:9)2012_alten09indexed","doi-asserted-by":"crossref","unstructured":"T. Altenkirch and P. Morris. Indexed Containers. In A. Pitts, editor,Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, pages 277-285. IEEE Computer Society, 2009.","DOI":"10.1109\/LICS.2009.33"},{"key":"10.2168\/LMCS-8(2:9)2012_atkey11refinement","doi-asserted-by":"crossref","unstructured":"R. Atkey, P. Johann, and N. Ghani. When Is a Type Refinement an Inductive Type? In M. Hofmann, editor,Foundations of Software Science and Computational Structures, volume 6604 ofLecture Notes in Computer Science, pages 72-87. Springer, 2011.","DOI":"10.1007\/978-3-642-19805-2_6"},{"key":"10.2168\/LMCS-8(2:9)2012_bghj07","doi-asserted-by":"crossref","unstructured":"R. Backhouse, J. Gibbons, R. Hinze, and J. Jeuring, editors.Datatype-Generic Programming, volume 4719 ofLecture Notes in Computer Science. Springer, 2007.","DOI":"10.1007\/978-3-540-76786-2"},{"key":"10.2168\/LMCS-8(2:9)2012_barr83toposes","unstructured":"M. Barr and C. Wells.Toposes, Triples and Theories. Springer, 1983."},{"issue":"4","key":"10.2168\/LMCS-8(2:9)2012_bdj03","first-page":"265","volume":"10","author":"M. Benke, P. Dybjer, and P. Jansson","year":"2003","journal-title":"Nordic Journal of Computing"},{"key":"10.2168\/LMCS-8(2:9)2012_bdm97","doi-asserted-by":"crossref","unstructured":"R. S. Bird and O. de Moor.Algebra of Programming. Prentice Hall, 1997.","DOI":"10.1007\/978-3-642-61455-2_12"},{"key":"10.2168\/LMCS-8(2:9)2012_brady03inductive","doi-asserted-by":"crossref","unstructured":"E. Brady, C. McBride, and J. McKinna. Inductive Families Need Not Store Their Indices. In S. Berardi, M. Coppo, and F. Damiani, editors,Types for Proofs and Programs, volume 3085 ofLecture Notes in Computer Science, pages 115-129. Springer, 2004.","DOI":"10.1007\/978-3-540-24849-1_8"},{"issue":"2","key":"10.2168\/LMCS-8(2:9)2012_clw93","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0022-4049(93)90035-R","volume":"84","author":"A. Carboni, S. Lack, and R. F. C. Walter","year":"1993","journal-title":"Journal of Pure and Applied Algebra"},{"key":"10.2168\/LMCS-8(2:9)2012_chapman10gentle","doi-asserted-by":"crossref","unstructured":"J. Chapman, P.-E. Dagand, C. McBride, and P. Morris. The gentle art of levitation. In S. Weirich, editor,Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP '10, pages 3-14. ACM, 2010.","DOI":"10.1145\/1863543.1863547"},{"key":"10.2168\/LMCS-8(2:9)2012_chuang06algebra","unstructured":"T.-R. Chuang and J.-L. Lin. An algebra of dependent data types. Technical Report TR-IIS-06-012, Institute of Information Science, Academia Sinica, Taiwan, 2006."},{"key":"10.2168\/LMCS-8(2:9)2012_cormen01intro","unstructured":"T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein.Introduction to Algorithms. MIT Press and McGraw-Hill, 2nd edition, 2001."},{"key":"10.2168\/LMCS-8(2:9)2012_DagandMcBride2012funOrn","doi-asserted-by":"crossref","unstructured":"P.-\u00c9. Dagand and C. McBride. Transporting functions across ornaments.The Computing Research Repository (CoRR), abs\/1201.4801, 2012.","DOI":"10.1145\/2364527.2364544"},{"key":"10.2168\/LMCS-8(2:9)2012_davies05practical","unstructured":"R. Davies.Practical Refinement-Type Checking. PhD thesis, Carnegie Mellon University, 2005."},{"key":"10.2168\/LMCS-8(2:9)2012_denney98refinement","doi-asserted-by":"crossref","unstructured":"E. Denney. Refinement types for specification. In D. Gries and W. P. de Roever, editors,Proceedings of the IFIP TC2\/WG2.2,2.3 International Conference on Programming Concepts and Methods, PROCOMET '98, pages 148-166. Chapman & Hall, Ltd., 1998.","DOI":"10.1007\/978-0-387-35358-6_13"},{"key":"10.2168\/LMCS-8(2:9)2012_dunfield07unified","unstructured":"J. Dunfield.A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, 2007."},{"issue":"4","key":"10.2168\/LMCS-8(2:9)2012_dybjer94inductive","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","journal-title":"Formal Aspects of Computing"},{"issue":"1-3","key":"10.2168\/LMCS-8(2:9)2012_dybjer03induction","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0168-0072(02)00096-9","volume":"124","author":"P. Dybjer and A. Setzer","year":"2003","journal-title":"Annals of Pure and Applied Logic"},{"issue":"1","key":"10.2168\/LMCS-8(2:9)2012_dybjer06indexed","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jlap.2005.07.001","volume":"66","author":"P. Dybjer and A. Setzer","year":"2006","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"10.2168\/LMCS-8(2:9)2012_freeman91refinement","doi-asserted-by":"crossref","unstructured":"T. Freeman and F. Pfenning. Refinement types for ML. In D. Wise, editor,Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, PLDI '91, pages 268-277. ACM, 1991.","DOI":"10.1145\/113445.113468"},{"key":"10.2168\/LMCS-8(2:9)2012_ghani10induction","doi-asserted-by":"crossref","unstructured":"N. Ghani, P. Johann, and C. Fumex. Fibrational induction rules for initial algebras. In A. Dawar and H. Veith, editors,Computer Science Logic, volume 6247 ofLecture Notes in Computer Science, pages 336-350. Springer, 2010.","DOI":"10.1007\/978-3-642-15205-4_27"},{"key":"10.2168\/LMCS-8(2:9)2012_gordon09principles","unstructured":"A. D. Gordon and C. Fournet. Principles and applications of refinement types. Technical Report MSR-TR-2009-147, Microsoft Research, 2009."},{"issue":"2","key":"10.2168\/LMCS-8(2:9)2012_hermida98structural","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1006\/inco.1998.2725","volume":"145","author":"C. Hermida and B. Jacobs","year":"1998","journal-title":"Information and Computation"},{"issue":"2","key":"10.2168\/LMCS-8(2:9)2012_jacobs93comprehension","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/0304-3975(93)90169-T","volume":"107","author":"B. Jacobs","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(2:9)2012_jacobs99book","unstructured":"B. Jacobs.Categorical Logic and Type Theory, volume 141 ofStudies in Logic and the Foundations of Mathematics. North Holland, 1999."},{"key":"10.2168\/LMCS-8(2:9)2012_kawaguchi09type","doi-asserted-by":"crossref","unstructured":"M. Kawaguchi, P. Rondon, and R. Jhala. Type-based data structure verification. In A. Diwan, editor,Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '09, pages 304-315. ACM, 2009.","DOI":"10.1145\/1542476.1542510"},{"key":"10.2168\/LMCS-8(2:9)2012_KoGibbons2011OAOAOO","doi-asserted-by":"publisher","DOI":"10.1145\/2036918.2036921"},{"key":"10.2168\/LMCS-8(2:9)2012_lovas10refinement","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:5)2010"},{"key":"10.2168\/LMCS-8(2:9)2012_malatesta12small","unstructured":"L. Malatesta, T. Altenkirch, N. Ghani, P. Hancock, and C. McBride. Small Induction Recursion, Indexed Containers and Dependent Polynomials are equivalent. Submitted for Publication, 2012."},{"key":"10.2168\/LMCS-8(2:9)2012_malcolm90","unstructured":"G. Malcolm.Algebraic Data Types and Program Transformation. PhD thesis, University of Groningen, 1990."},{"key":"10.2168\/LMCS-8(2:9)2012_mcbride10ornaments","unstructured":"C. McBride. Ornamental algebras, algebraic ornaments.Journal of Functional Programming, 2011. To appear."},{"issue":"5","key":"10.2168\/LMCS-8(2:9)2012_meertens92paramorphism","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/BF01211391","volume":"4","author":"L. Meertens","year":"1992","journal-title":"Formal Aspects of Computing"},{"key":"10.2168\/LMCS-8(2:9)2012_agda10","unstructured":"U. Norell.Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology and G\u00f6teborg University, 2007."},{"key":"10.2168\/LMCS-8(2:9)2012_pfenning93refinement","unstructured":"F. Pfenning. Refinement types for logical frameworks. In H. Geuvers, editor,Informal Proceedings of the Workshop on Types for Proofs and Programs, pages 285-299, 1993."},{"issue":"9","key":"10.2168\/LMCS-8(2:9)2012_rushby98subtypes","first-page":"709","volume":"24","author":"J. Rushby, S. Owre, and N. Shankar","year":"1998","journal-title":"IEEE Transactions on Software Engineering 1998"},{"key":"10.2168\/LMCS-8(2:9)2012_xi00dependently","unstructured":"H. Xi. Dependently typed data structures. Unpublished Note, Revision after WAAAPL '99, 2000."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/957\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/957\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:52Z","timestamp":1681243192000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/957"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,4]]},"references-count":37,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:9)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1205.2492","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1205.2492","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,6,4]]},"article-number":"957"}}