{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:21Z","timestamp":1747173441609,"version":"3.40.5"},"reference-count":48,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2021,12,10]],"date-time":"2021-12-10T00:00:00Z","timestamp":1639094400000},"content-version":"unspecified","delay-in-days":192,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2021,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Guided by Tarksi\u2019s fixpoint theorem in order theory, we show how to derive monotone recursive types with constant-time <jats:italic>roll<\/jats:italic> and <jats:italic>unroll<\/jats:italic> operations within Cedille, an impredicative, constructive, and logically consistent pure typed lambda calculus. This derivation takes place within the preorder on Cedille types induced by <jats:italic>type inclusions<\/jats:italic>, a notion which is expressible within the theory itself. As applications, we use monotone recursive types to generically derive two recursive representations of data in lambda calculus, the Parigot and Scott encoding. For both encodings, we prove induction and examine the computational and extensional properties of their destructor, iterator, and primitive recursor in Cedille. For our Scott encoding in particular, we translate into Cedille a construction due to Lepigre and Raffalli (2019) that equips Scott naturals with primitive recursion, then extend this construction to derive a generic induction principle. This allows us to give efficient and provably unique (up to function extensionality) solutions for the iteration and primitive recursion schemes for Scott-encoded data.<\/jats:p>","DOI":"10.1017\/s0960129521000402","type":"journal-article","created":{"date-parts":[[2021,12,10]],"date-time":"2021-12-10T06:52:45Z","timestamp":1639119165000},"page":"682-745","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Monotone recursive types and recursive data representations in Cedille"],"prefix":"10.1017","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5434-5018","authenticated-orcid":false,"given":"Christopher","family":"Jenkins","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,12,10]]},"reference":[{"key":"S0960129521000402_ref28","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151642"},{"volume-title":"Perspectives in Logic","year":"2013","author":"Barendregt","key":"S0960129521000402_ref7"},{"key":"S0960129521000402_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"S0960129521000402_ref47","first-page":"5","article-title":"Primitive (co)recursion and course-of-value (co)iteration, categorically","volume":"10","author":"Uustalu","year":"1999","journal-title":"Informatica"},{"key":"S0960129521000402_ref19","unstructured":"[19] Kleene, S. (1965). Classical extensions of intuitionistic mathematics. In: Bar-Hillel, Y. (ed.), LMPS 2. North-Holland Publishing Company, 31\u201344."},{"key":"S0960129521000402_ref48","unstructured":"[48] Wadler, P. (1990). Recursive types for free! Unpublished manuscript."},{"key":"S0960129521000402_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/10703163_20"},{"key":"S0960129521000402_ref39","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000053"},{"key":"S0960129521000402_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/301631.301641"},{"key":"S0960129521000402_ref18","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:12)2012"},{"key":"S0960129521000402_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054285"},{"key":"S0960129521000402_ref34","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"S0960129521000402_ref43","unstructured":"[43] Stump, A. and Jenkins, C. (2021). Syntax and semantics of Cedille. CoRR, abs\/1806.04709."},{"key":"S0960129521000402_ref31","doi-asserted-by":"crossref","unstructured":"[31] Parigot, M. (1989). On the representation of data in lambda-calculus. In B\u00f6rger, E., B\u00fcning, H. and Richter, M. (eds.), Computer Science Logic (CSL), vol. 440. Lecture Notes in Computer Science. Springer, 309\u2013321.","DOI":"10.1007\/3-540-52753-2_47"},{"key":"S0960129521000402_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_16"},{"key":"S0960129521000402_ref10","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/0304-3975(79)90014-8","article-title":"A discrimination algorithm inside \u03bb-\u03b2-calculus","volume":"8","author":"B\u00f6hm","year":"1979","journal-title":"Theoretical Computer Science"},{"key":"S0960129521000402_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36576-1_2"},{"key":"S0960129521000402_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000150"},{"key":"S0960129521000402_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(82)90065-5"},{"key":"S0960129521000402_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"volume-title":"A system of functional abstraction","year":"1962","author":"Scott","key":"S0960129521000402_ref36"},{"key":"S0960129521000402_ref23","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1983.50"},{"volume-title":"Types and Programming Languages","year":"2002","author":"Pierce","key":"S0960129521000402_ref33"},{"key":"S0960129521000402_ref20","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210048"},{"key":"S0960129521000402_ref17","unstructured":"[17] Geuvers, H. (2014). The Church-Scott representation of inductive and coinductive data. Unpublished manuscript."},{"key":"S0960129521000402_ref45","unstructured":"[45] The Agda Team. (2021). The Agda standard library, v1.5. https:\/\/github.com\/agda\/agda-stdlibhttps:\/\/github.com\/agda\/agda-stdlib."},{"key":"S0960129521000402_ref15","unstructured":"[15] Geuvers, H. (1992). Inductive and coinductive types with iteration and recursion. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, Bastad. Bastad, Chalmers University of Technology, 183\u2013207."},{"key":"S0960129521000402_ref41","unstructured":"[41] Stump, A. (2018b). Syntax and typing for Cedille core. CoRR, abs\/1811.01318."},{"key":"S0960129521000402_ref46","unstructured":"[46] Ullrich, M. (2020). Generating induction principles for nested inductive types in MetaCoq. Bachelor\u2019s thesis."},{"key":"S0960129521000402_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_14"},{"key":"S0960129521000402_ref27","unstructured":"[27] The Coq Development Team. (2018). The Coq proof assistant reference manual. LogiCal Project. Version 8.7.2."},{"key":"S0960129521000402_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000034"},{"key":"S0960129521000402_ref26","doi-asserted-by":"publisher","DOI":"10.1023\/A:1020831825964"},{"key":"S0960129521000402_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19027-9_10"},{"volume-title":"Lectures on the Curry-Howard Isomorphism, Vol. 149 (Studies in Logic and the Foundations of Mathematics)","year":"2006","author":"S\u00f8rensen","key":"S0960129521000402_ref37"},{"key":"S0960129521000402_ref3","unstructured":"[3] Abel, A. (2010). MiniAgda: Integrating sized and dependent types. In: Komendantskaya, E., Bove, A. and Niqui, M. (eds.) Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010, vol. 5. EPiC Series. EasyChair, 18\u201333."},{"key":"S0960129521000402_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_25"},{"key":"S0960129521000402_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"S0960129521000402_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2018.03.002"},{"key":"S0960129521000402_ref12","unstructured":"[12] Dybjer, P. and Palmgren, E. (2016). Intuitionistic type theory. In: E. N. Zalta (ed.), The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2016 edition."},{"key":"S0960129521000402_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3285955"},{"key":"S0960129521000402_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.017"},{"key":"S0960129521000402_ref38","doi-asserted-by":"crossref","unstructured":"[38] Splawski, Z. and Urzyczyn, P. (1999). Type fixpoints: Iteration vs. recursion. In: R\u00e9my, D. and Lee, P. (eds.), Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming (ICFP 1999), Paris, France, September 27-29, 1999. ACM, 102\u2013113.","DOI":"10.1145\/317765.317789"},{"key":"S0960129521000402_ref44","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S0960129521000402_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90042-E"},{"key":"S0960129521000402_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"S0960129521000402_ref1","unstructured":"[1] Abadi, M. , Cardelli, L. and Plotkin, G. (1993). Types for the Scott numerals. Unpublished note."},{"key":"S0960129521000402_ref14","doi-asserted-by":"crossref","unstructured":"[14] Firsov, D. and Stump, A. (2018). Generic derivation of induction for impredicative encodings in cedille. In: Andronick, J. and Felty, A. P. (eds.), Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018. ACM, 215\u2013227.","DOI":"10.1145\/3176245.3167087"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129521000402","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,31]],"date-time":"2022-01-31T11:36:59Z","timestamp":1643629019000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129521000402\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":48,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,6]]}},"alternative-id":["S0960129521000402"],"URL":"https:\/\/doi.org\/10.1017\/s0960129521000402","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2021,6]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}