{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T05:39:55Z","timestamp":1791437995789,"version":"4.3.3"},"reference-count":16,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T00:00:00Z","timestamp":1416441600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,1]]},"abstract":"<jats:p>Induction recursion offers the possibility of a clean, simple and yet powerful meta-language for the type system of a dependently typed programming language. At its crux, induction recursion allows us to define a universe, that is a set<jats:italic>U<\/jats:italic>of<jats:italic>codes<\/jats:italic>and a decoding function<jats:italic>T : U \u2192 D<\/jats:italic>which assigns to every code<jats:italic>u : U<\/jats:italic>, a value<jats:italic>T, u<\/jats:italic>of some type<jats:italic>D, e.g.<\/jats:italic>the large type Set of small types or sets. The name induction recursion refers to the build-up of codes in<jats:italic>U<\/jats:italic>using inductive clauses, simultaneously with the definition of the function<jats:italic>T<\/jats:italic>, by structural recursion on codes.<\/jats:p><jats:p>Our contribution is to (i) bring out explicitly algebraic structure which is less visible in the original type-theoretic presentation \u2013 in particular showing how containers and monads play a pivotal role within induction recursion; and (ii) use these structures to present a clean and high level definition of induction recursion suitable for use in functional programming.<\/jats:p>","DOI":"10.1017\/s0960129514000127","type":"journal-article","created":{"date-parts":[[2014,11,20]],"date-time":"2014-11-20T10:23:27Z","timestamp":1416479007000},"page":"89-113","source":"Crossref","is-referenced-by-count":2,"title":["Containers, monads and induction recursion"],"prefix":"10.1017","volume":"26","author":[{"given":"NEIL","family":"GHANI","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"PETER","family":"HANCOCK","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,11,20]]},"reference":[{"key":"S0960129514000127_ref13","volume-title":"Categories for the Working Mathematician","author":"Mac Lane","year":"1998"},{"key":"S0960129514000127_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.07.001"},{"key":"S0960129514000127_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_11"},{"key":"S0960129514000127_ref2","doi-asserted-by":"crossref","unstructured":"Altenkirch T. , Levy P. and Staton S. (2010) Higher order containers. Computability in Europe.","DOI":"10.1007\/978-3-642-13962-8_2"},{"key":"S0960129514000127_ref16","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635159"},{"key":"S0960129514000127_ref15","doi-asserted-by":"crossref","unstructured":"Morris P. and Altenkirch T. (2009) Indexed containers. In: 24th IEEE Symposium in Logic in Computer Science (LICS 2009).","DOI":"10.1109\/LICS.2009.33"},{"key":"S0960129514000127_ref5","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"S0960129514000127_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"S0960129514000127_ref14","first-page":"73","volume-title":"Logic Colloquium '73","author":"Martin-L\u00f6f","year":"1973"},{"key":"S0960129514000127_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"S0960129514000127_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_6"},{"key":"S0960129514000127_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00349-2"},{"key":"S0960129514000127_ref12","doi-asserted-by":"crossref","unstructured":"Kahle R. and Setzer A. (2010) An extended predicative definition of the Mahlo universe. In: Ways of ProofTheory. Festschrift on the occasion of Wolfram Pohler's retirement, Ontos Verlag.","DOI":"10.1515\/9783110324907.315"},{"key":"S0960129514000127_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0960129514000127_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"S0960129514000127_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45504-3_7"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000127","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T16:11:18Z","timestamp":1566058278000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000127\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,20]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,1]]}},"alternative-id":["S0960129514000127"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000127","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,20]]}}}