{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:53:11Z","timestamp":1776891191858,"version":"3.51.2"},"reference-count":67,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,9,16]],"date-time":"2022-09-16T00:00:00Z","timestamp":1663286400000},"content-version":"unspecified","delay-in-days":258,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Many programmers use dependently typed languages such as Coq to machine-verify high-assurance software. However, existing compilers for these languages provide no guarantees after compiling, nor when linking after compilation.\n                    <jats:italic>Type-preserving compilers<\/jats:italic>\n                    preserve guarantees encoded in types and then use type checking to verify compiled code and ensure safe linking with external code. Unfortunately, standard compiler passes do not preserve the dependent typing of commonly used (intensional) type theories. This is because assumptions valid in simpler type systems no longer hold, and intensional dependent type systems are highly sensitive to syntactic changes, including compilation. We develop an A-normal form (ANF) translation with join-point optimization\u2014a standard translation for making control flow explicit in functional languages\u2014from the Extended Calculus of Constructions (ECC) with dependent elimination of booleans and natural numbers (a representative subset of Coq). Our dependently typed target language has equality reflection, allowing the type system to encode semantic equality of terms. This is key to proving type preservation and correctness of separate compilation for this translation. This is the first ANF translation for dependent types. Unlike related translations, it supports the universe hierarchy, and does not rely on parametricity or impredicativity.\n                  <\/jats:p>","DOI":"10.1017\/s0956796822000090","type":"journal-article","created":{"date-parts":[[2022,9,16]],"date-time":"2022-09-16T05:33:40Z","timestamp":1663306420000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":2,"title":["ANF preserves dependent types up to extensional equality"],"prefix":"10.46298","volume":"32","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0325-3305","authenticated-orcid":false,"given":"PAULETTE","family":"KORONKEVICH","sequence":"first","affiliation":[]},{"given":"RAMON","family":"RAKOW","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7424-572X","authenticated-orcid":false,"given":"AMAL","family":"AHMED","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6402-4840","authenticated-orcid":false,"given":"WILLIAM J.","family":"BOWMAN","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2022,9,16]]},"reference":[{"key":"S0956796822000090_ref14","unstructured":"Bowman, W. J. & Ahmed, A. (2018) Parametric Closure Conversion for CIC. Available at: https:\/\/web.archive.org\/web\/20210423031005\/https:\/\/www.williamjbowman.com\/resources\/wjb2018-techreport-parametric-cc-cic.pdf."},{"key":"S0956796822000090_ref22","doi-asserted-by":"crossref","DOI":"10.1145\/3236764","article-title":"Handling delimited continuations with dependent types","author":"Cong","year":"2018","journal-title":"Proc. ACM Program. Lang. (PACMPL). 2(ICFP)"},{"key":"S0956796822000090_ref63","doi-asserted-by":"crossref","unstructured":"Thielecke, H. (2003) From control effects to typed continuation passing. In Symposium on Principles of Programming Languages (POPL). 10.1145\/640128.604144.","DOI":"10.1145\/604131.604144"},{"key":"S0956796822000090_ref67","doi-asserted-by":"crossref","unstructured":"Xi, H. & Harper, R. (2001) A dependently typed assembly language. In International Conference on Functional Programming (ICFP). 10.1145\/507635.507657.","DOI":"10.1145\/507635.507657"},{"key":"S0956796822000090_ref15","article-title":"Type-preserving CPS translation of","volume":"2","author":"Bowman","year":"2018","journal-title":"Proc. ACM Program. Lang. (PACMPL)."},{"key":"S0956796822000090_ref46","doi-asserted-by":"crossref","unstructured":"P\u00e9drot, P.-M. & Tabareau, N. (2019) The fire triangle: How to mix substitution, dependent elimination, and effects. In Symposium on Principles of Programming Languages (POPL). 10.1145\/3371126.","DOI":"10.1145\/3371126"},{"key":"S0956796822000090_ref17","unstructured":"Chan, J. (2021) An Analysis of An Analysis of Girard\u2019s Paradox. Available at: https:\/\/web.archive.org\/web\/20220429152422\/https:\/\/ionathan.ch\/\/2021\/11\/24\/inconsisten- cies.html."},{"key":"S0956796822000090_ref65","unstructured":"V\u00e1k\u00e1r, M. (2017) In Search of Effectful Dependent Types. Ph.D. thesis. Oxford University. Available at: http:\/\/arxiv.org\/abs\/1706.07997."},{"key":"S0956796822000090_ref39","doi-asserted-by":"crossref","unstructured":"Miquey, \u00e9. (2017) A classical sequent calculus with dependent types. In European Symposium on Programming (ESOP). 10.1007\/978-3-662-54434-1_29.","DOI":"10.1007\/978-3-662-54434-1_29"},{"key":"S0956796822000090_ref19","doi-asserted-by":"crossref","unstructured":"Chen, J. , Hawblitzel, C. , Perry, F. , Emmi, M. , Condit, J. , Coetzee, D. & Pratikaki, P. (2008) Type-preserving compilation for large-scale optimizing object-oriented compilers. In International Conference on Programming Language Design and Implementation (PLDI). 10.1145\/1375581.1375604.","DOI":"10.1145\/1375581.1375604"},{"key":"S0956796822000090_ref49","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1017\/CBO9780511526619.007","volume-title":"Semantics and Logics of Computation","author":"Pitts","year":"1997"},{"key":"S0956796822000090_ref61","unstructured":"Stump, A. & Jenkins, C. (2018) Syntax and Semantics of Cedille. Available at: http:\/\/arxiv.org\/pdf\/1806.04709v3."},{"key":"S0956796822000090_ref30","unstructured":"Herbelin, H. (2009) On a few open problems of the calculus of inductive constructions and on their practical consequences. Updated 2010. Available at: https:\/\/web.archive.org\/web\/20181125182737\/http:\/\/pauillac.inria.fr\/ herbelin\/talks\/cic.pdf."},{"key":"S0956796822000090_ref7","doi-asserted-by":"crossref","unstructured":"Barthe, G. , Gr\u00e9goire, B. & Zanella-B\u00e9guelin, S. (2009) Formal certification of code-based cryptographic proofs. In Symposium on Principles of Programming Languages (POPL). 10.1145\/1480881.1480894.","DOI":"10.1145\/1480881.1480894"},{"key":"S0956796822000090_ref47","doi-asserted-by":"crossref","unstructured":"Perconti, J. T. & Ahmed, A. (2014) Verifying an open compiler using multi-language semantics. In European Symposium on Programming (ESOP). 10.1007\/978-3-642-54833-8_8.","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"S0956796822000090_ref50","doi-asserted-by":"crossref","DOI":"10.1145\/141471.141563","article-title":"Reasoning about programs in continuation-Passing style","author":"Sabry","year":"1992","journal-title":"LISP and Functional Programming"},{"key":"S0956796822000090_ref37","unstructured":"Luo, Z. (1990) An Extended Calculus of Constructions. Ph.D. thesis. University of Edinburgh. Available at: http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/90\/ECS-LFCS-90-118\/."},{"key":"S0956796822000090_ref32","unstructured":"Huet, G. (1986) Formal Structures for Computation and Deduction. Technical report. Available at: http:\/\/web.archive.org\/web\/20220408113829\/http:\/\/pauillac.inria.fr\/ huet\/PUBLIC\/Formal_Structures.ps.gz."},{"key":"S0956796822000090_ref25","doi-asserted-by":"crossref","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inf. Comput."},{"key":"S0956796822000090_ref24","first-page":"1","article-title":"Compiling with continuations, or without? whatever","volume":"3","author":"Cong","year":"2019","journal-title":"PACMPL"},{"key":"S0956796822000090_ref41","doi-asserted-by":"crossref","unstructured":"Necula, G. C. (1997) Proof-carrying code. In Symposium on Principles of Programming Languages (POPL). 10.1145\/263699.263712.","DOI":"10.1145\/263699.263712"},{"key":"S0956796822000090_ref40","doi-asserted-by":"crossref","DOI":"10.1145\/319301.319345","article-title":"From system F to typed assembly language","volume":"21","author":"Morrisett","year":"1999","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)."},{"key":"S0956796822000090_ref20","doi-asserted-by":"crossref","unstructured":"Chlipala, A. (2007) A certified type-preserving compiler from lambda calculus to assembly language. In International Conference on Programming Language Design and Implementation (PLDI). 10.1145\/1250734.1250742.","DOI":"10.1145\/1250734.1250742"},{"key":"S0956796822000090_ref44","doi-asserted-by":"crossref","unstructured":"Patterson, D. , Perconti, J. , Dimoulas, C. & Ahmed, A. (2017) FunTAL: Reasonably mixing a functional language with assembly. In International Conference on Programming Language Design and Implementation (PLDI). 10.1145\/3062341.3062347.","DOI":"10.1145\/3062341.3062347"},{"key":"S0956796822000090_ref57","doi-asserted-by":"crossref","DOI":"10.1145\/1053468.1053469","article-title":"A type system for certified binaries","volume":"27","author":"Shao","year":"2005","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"S0956796822000090_ref38","doi-asserted-by":"crossref","unstructured":"Maurer, L. , Downen, P. , Ariola, Z. M. & Peyton Jones, S. (2017) Compiling without continuations. In International Conference on Programming Language Design and Implementation (PLDI). 10.1145\/3062341.3062380.","DOI":"10.1145\/3062341.3062380"},{"key":"S0956796822000090_ref52","unstructured":"Saffrich, H. & Thiemann, P. (2020) Relating functional and imperative session types. Available at: https:\/\/arxiv.org\/abs\/2010.08261."},{"key":"S0956796822000090_ref58","unstructured":"Sozeau, M. (2008) Un environnement pour la programmation avec types d\u00e9pendants. (An Environment for Programming with Dependent Types). Ph.D. thesis. Orsay, France: University of Paris-Sud. Available at: https:\/\/tel.archives-ouvertes.fr\/tel-00640052."},{"key":"S0956796822000090_ref51","doi-asserted-by":"crossref","DOI":"10.1145\/267959.269968","article-title":"A reflection on call-by-value","volume":"19","author":"Sabry","year":"1997","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"S0956796822000090_ref59","unstructured":"Stecklein, J. M. , Dabney, J. , Dick, B. , Haskins, B. , Lovell, R. & Moroney, G. (2004) Error Cost Escalation through the Project Life Cycle. Technical report. NASA. Available at: https:\/\/ntrs.nasa.gov\/search.jsp?R=20100036670."},{"key":"S0956796822000090_ref62","doi-asserted-by":"crossref","unstructured":"Tarditi, D. , Morrisett, G. , Cheng, P. , Stone, C. , Harper, R. & Lee, P. (1996) TIL: A type-directed optimizing compiler for ML. In International Conference on Programming Language Design and Implementation (PLDI). 10.1145\/231379.231414.","DOI":"10.21236\/ADA306265"},{"key":"S0956796822000090_ref43","doi-asserted-by":"crossref","unstructured":"Oury, N. (2005) Extensionality in the calculus of constructions. In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22\u201325, 2005, Proceedings. Springer, pp. 278\u2013293. 10.1007\/11541868_18.","DOI":"10.1007\/11541868_18"},{"key":"S0956796822000090_ref10","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S1571-0661(05)80280-4","article-title":"Monads, effects and transformations","volume":"26","author":"Benton","year":"1999","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"S0956796822000090_ref27","doi-asserted-by":"crossref","unstructured":"Gordon, A. D. (1995) Bisimilarity as a theory of functional programming. In Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 1995, Tulane University, New Orleans, LA, USA, March 29\u2013April 1, 1995. Elsevier, pp. 232\u2013252. 10.1016\/S1571-0661(04)80013-6.","DOI":"10.1016\/S1571-0661(04)80013-6"},{"key":"S0956796822000090_ref64","unstructured":"Timany, A. & Sozeau, M. (2017) Consistency of the predicative calculus of cumulative inductive constructions (pCuIC). arXiv preprint arXiv:1710.03912. Available at: https:\/\/arxiv.org\/abs\/1710.03912."},{"key":"S0956796822000090_ref42","doi-asserted-by":"crossref","unstructured":"Necula, G. C. & Rahul, S. P. (2001) Oracle-based checking of untrusted software. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17\u201319, 2001. ACM, pp. 142\u2013154. 10.1145\/360204.360216.","DOI":"10.1145\/373243.360216"},{"key":"S0956796822000090_ref18","unstructured":"Chan, J. & Bowman, W. J. (2020) Practical sized typing for coq. Available at: https:\/\/arxiv.org\/abs\/1912.05601."},{"key":"S0956796822000090_ref5","unstructured":"Anand, A. , Appel, A. W. , Morrisett, G. , Paraskevopoulou, Z. , Pollack, R. , B\u00e9langer, O. S. , Sozeau, M. & Weaver, M. (2017) CertiCoq: A verified compiler for Coq. In International Workshop on Coq for Programming Languages (CoqPL). Available at: http:\/\/www.cs.princeton.edu\/ appel\/papers\/certicoq-coqpl.pdf."},{"key":"S0956796822000090_ref54","doi-asserted-by":"crossref","unstructured":"Severi, P. & Poll, E. (1994) Pure type systems with definitions. In International Symposium Logical Foundations of Computer Science (LFCS). 10.1007\/3-540-58140-5_30.","DOI":"10.1007\/3-540-58140-5_30"},{"key":"S0956796822000090_ref48","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S. L. (1996) Compiling Haskell by program transformation: A report from the trenches. In European Symposium on Programming (ESOP). 10.1007\/3-540-61055-3_27.","DOI":"10.1007\/3-540-61055-3_27"},{"key":"S0956796822000090_ref29","unstructured":"Gu, R. , Shao, Z. , Chen, H. , Wu, X. N. , Kim, J. , Sj\u00d6berg, V. & Costanzo, D. (2016) CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Symposium on Operating Systems Design and Implementation (OSDI). Available at: https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu. Herbelin, H. (2005) On the degeneracy of $\\Sigma$ -types in presence of computational classical logic. In International Conference on Typed Lambda Calculi and Applications. 10.1007\/11417170_16."},{"key":"S0956796822000090_ref28","doi-asserted-by":"crossref","unstructured":"Gu, R. , Koenig, J. , Ramananandro, T. , Shao, Z. , Wu, X. n. , Weng, S.-c. , Zhang, H. & Guo, Y. (2015) Deep specifications and certified abstraction layers. In Symposium on Principles of Programming Languages (POPL). 10.1145\/2775051.2676975.","DOI":"10.1145\/2676726.2676975"},{"key":"S0956796822000090_ref53","doi-asserted-by":"crossref","unstructured":"Sarkar, S. , Pientka, B. & Crary, K. (2005) Small proof witnesses for LF. In International Conference Logic Programming (ICLP). 10.1007\/11562931_29.","DOI":"10.1007\/11562931_29"},{"key":"S0956796822000090_ref4","doi-asserted-by":"crossref","unstructured":"Ahmed, A. & Blume, M. (2011) An Equivalence-Preserving CPS Translation via Multi-Language Semantics (Technical Appendix). Technical report. Available at: http:\/\/www.ccs.neu.edu\/home\/amal\/papers\/epc-tr.pdf.","DOI":"10.1145\/2034773.2034830"},{"key":"S0956796822000090_ref36","unstructured":"Levy, P. B. (2012) Call-By-Push-Value. Available at: https:\/\/www.worldcat.org\/oclc\/7330961929."},{"key":"S0956796822000090_ref12","doi-asserted-by":"crossref","unstructured":"Boulier, S. , P\u00e9drot, P. & Tabareau, N. (2017) The next 700 syntactical models of type theory. In Conference on Certified Programs and Proofs (CPP). 10.1145\/3018610.3018620.","DOI":"10.1145\/3018610.3018620"},{"key":"S0956796822000090_ref11","doi-asserted-by":"crossref","unstructured":"Benton, N. , Kennedy, A. & Russell, G. (1998) Compiling standard ML to Java bytecodes. In International Conference on Functional Programming (ICFP). 10.1145\/289423.289435.","DOI":"10.1145\/289423.289435"},{"key":"S0956796822000090_ref13","unstructured":"Boutillier, P. (2012) A relaxation of Coq\u2019s guard condition. Journ\u00e9es Francophones des langages applicatifs (JFLA). Available at: https:\/\/hal.archives-ouvertes.fr\/hal-00651780."},{"key":"S0956796822000090_ref16","unstructured":"Briski, K. A. , Chitale, P. , Hamilton, V. , Pratt, A. , Starr, B. , Veroulis, J. & Villard, B. (2008) Minimizing Code Defects to Improve Software Quality and Lower Development Costs. Development Solutions. IBM. Available at: ftp:\/\/ftp.software.ibm.com\/software\/rational\/info\/do-more\/RAW14109USEN.pdf."},{"key":"S0956796822000090_ref34","doi-asserted-by":"crossref","DOI":"10.1145\/3495528","article-title":"Gradualizing the calculus of inductive constructions","author":"Lennon-Bertrand","year":"2022","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"S0956796822000090_ref33","doi-asserted-by":"crossref","unstructured":"Kennedy, A. (2007) Compiling with continuations, continued. In International Conference on Functional Programming (ICFP). 10.1145\/1291220.1291179.","DOI":"10.1145\/1291151.1291179"},{"key":"S0956796822000090_ref2","article-title":"Verified Compilers for a Multi-language World","author":"Ahmed","year":"2015","journal-title":"Summit on Advances in Programming Languages (SNAPL)."},{"key":"S0956796822000090_ref55","unstructured":"Shao, Z. (1997) An Overview of the FLINT\/ML Compiler. Available at: https:\/\/web.archive.org\/web\/20161125002746\/http:\/\/cs.bc.edu\/ muller\/TIC97\/\/Shao.ps.gz."},{"key":"S0956796822000090_ref1","unstructured":"Ahman, D. (2017) Fibred Computational Effects. Ph.D. thesis. University of Edinburgh. Available at: http:\/\/arxiv.org\/abs\/1710.02594."},{"key":"S0956796822000090_ref66","article-title":"A concurrent logical framework: The propositional fragment","author":"Watkins","year":"2003","journal-title":"International Workshop on Types for Proofs and Programs (TYPES)."},{"key":"S0956796822000090_ref8","doi-asserted-by":"crossref","DOI":"10.1023\/A:1010000206149","article-title":"CPS translations and applications: The cube and beyond","volume":"12","author":"Barthe","year":"1999","journal-title":"Higher-Order Symb. Comput."},{"key":"S0956796822000090_ref21","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala","year":"2013"},{"key":"S0956796822000090_ref3","doi-asserted-by":"crossref","unstructured":"Ahmed, A. & Blume, M. (2011) An equivalence-preserving CPS translation via multi-language semantics. In International Conference on Functional Programming (ICFP). 10.1145\/2034773.2034830.","DOI":"10.1145\/2034773.2034830"},{"key":"S0956796822000090_ref56","doi-asserted-by":"crossref","unstructured":"Shao, Z. , League, C. & Monnier, S. (1998) Implementing typed intermediate languages. In International Conference on Functional Programming (ICFP). 10.1145\/289423.289460.","DOI":"10.1145\/289423.289460"},{"key":"S0956796822000090_ref35","article-title":"A formally verified compiler back-end","volume":"43","author":"Leroy","year":"2009","journal-title":"J. Autom. Reas."},{"key":"S0956796822000090_ref45","unstructured":"P\u00e9drot, P. (2017) A parametric CPS to sprinkle CIC with classical reasoning. In Workshop on Syntax and Semantics of Low-Level Languages. Available at: https:\/\/web.archive.org\/web\/20220122222238\/https:\/\/www.cs.bham.ac.uk\/zeilbern\/lola2017\/abstracts\/LOLA_2017_paper_5.pdf."},{"key":"S0956796822000090_ref60","doi-asserted-by":"crossref","unstructured":"Stewart, G. , Beringer, L. , Cuellar, S. & Appel, A. W. (2015) Compositional CompCert. In Symposium on Principles of Programming Languages (POPL). 10.1145\/2676726.2676985.","DOI":"10.1145\/2676726.2676985"},{"key":"S0956796822000090_ref31","doi-asserted-by":"crossref","unstructured":"Herbelin, H. (2012) A constructive proof of dependent choice, compatible with classical logic. In Symposium on Logic in Computer Science (LICS). 10.1109\/lics.2012.47.","DOI":"10.1109\/LICS.2012.47"},{"key":"S0956796822000090_ref6","doi-asserted-by":"crossref","DOI":"10.1145\/2701415","article-title":"Verification of a cryptographic primitive: SHA-256","volume":"37","author":"Appel","year":"2015","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)."},{"key":"S0956796822000090_ref26","doi-asserted-by":"crossref","unstructured":"Flanagan, C. , Sabry, A. , Duba, B. F. & Felleisen, M. (1993) The essence of compiling with continuations. In International Conference on Programming Language Design and Implementation (PLDI). 10.1145\/155090.155113.","DOI":"10.1145\/155090.155113"},{"key":"S0956796822000090_ref9","article-title":"CPS translating inductive and coinductive types","author":"Barthe","year":"2002","journal-title":"Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM)."},{"key":"S0956796822000090_ref23","unstructured":"Cong, Y. & Asai, K. (2018b) Shifting and resetting in the calculus of constructions. In International Symposium on Trends in Functional Programming (TFP). Available at: https:\/\/sites.google.com\/site\/youyoucong212\/tfp-2018."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796822000090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:17:50Z","timestamp":1776889070000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796822000090\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"references-count":67,"alternative-id":["S0956796822000090"],"URL":"https:\/\/doi.org\/10.1017\/s0956796822000090","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. 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 (https:\/\/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"}],"article-number":"e12"}}