{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:05:49Z","timestamp":1750089949451,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":31,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819983100"},{"type":"electronic","value":"9789819983117"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-981-99-8311-7_7","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T07:02:17Z","timestamp":1700636537000},"page":"135-154","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Fresh Look at\u00a0Commutativity: Free Algebraic Structures via\u00a0Fresh Lists"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0502-391X","authenticated-orcid":false,"given":"Clemens","family":"Kupke","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6157-9288","authenticated-orcid":false,"given":"Fredrik Nordvall","family":"Forsberg","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-1249-254X","authenticated-orcid":false,"given":"Sean","family":"Watters","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36576-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"M Abbott","year":"2003","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Categories of containers. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 23\u201338. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36576-1_2"},{"key":"7_CR2","unstructured":"The Agda Community: Agda standard library (2023). https:\/\/github.com\/agda\/agda-stdlib"},{"issue":"1","key":"7_CR3","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/s10817-022-09655-x","volume":"67","author":"AW Appel","year":"2023","unstructured":"Appel, A.W., Leroy, X.: Efficient extensional binary tries. J. Autom. Reason. 67(1), 8 (2023). https:\/\/doi.org\/10.1007\/s10817-022-09655-x","journal-title":"J. Autom. Reason."},{"issue":"2","key":"7_CR4","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13(2), 261\u2013293 (2003). https:\/\/doi.org\/10.1017\/S0956796802004501","journal-title":"J. Funct. Program."},{"issue":"5","key":"7_CR5","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1016\/j.ansens.2003.01.001","volume":"36","author":"D Bessis","year":"2003","unstructured":"Bessis, D.: The dual braid monoid. Annales scientifiques de l\u2019Ecole normale sup\u00e9rieure 36(5), 647\u2013683 (2003). https:\/\/doi.org\/10.1016\/j.ansens.2003.01.001","journal-title":"Annales scientifiques de l\u2019Ecole normale sup\u00e9rieure"},{"issue":"4","key":"7_CR6","first-page":"319","volume":"1","author":"WD Blizard","year":"1991","unstructured":"Blizard, W.D.: The development of multiset theory. Modern Logic 1(4), 319\u2013352 (1991)","journal-title":"Modern Logic"},{"issue":"3","key":"7_CR7","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1023\/a:1007822931408","volume":"13","author":"KS Brown","year":"2000","unstructured":"Brown, K.S.: Semigroups, rings, and Markov chains. J. Theor. Probab. 13(3), 871\u2013938 (2000). https:\/\/doi.org\/10.1023\/a:1007822931408","journal-title":"J. Theor. Probab."},{"key":"7_CR8","doi-asserted-by":"publisher","unstructured":"Bunkenburg, A.: The Boom hierarchy. In: O\u2019Donnell, J.T., Hammond, K. (eds.) Proceedings of the 1993 Glasgow Workshop on Functional Programming, pp. 1\u20138. Springer (1994). https:\/\/doi.org\/10.1007\/978-1-4471-3236-3_1","DOI":"10.1007\/978-1-4471-3236-3_1"},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Choudhury, V., Fiore, M.: Free commutative monoids in Homotopy Type Theory. In: Hsu, J., Tasson, C. (eds.) Mathematical Foundations of Programming Semantics (MFPS \u201922). Electronic Notes in Theoretical Informatics and Computer Science, vol. 1 (2023). https:\/\/doi.org\/10.46298\/entics.10492","DOI":"10.46298\/entics.10492"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Choudhury, V., Karwowski, J., Sabry, A.: Symmetries in reversible programming: From symmetric rig groupoids to reversible programming languages. In: Proceedings of the ACM on Programming Languages 6(POPL), pp. 1\u201332 (2022). https:\/\/doi.org\/10.1145\/3498667","DOI":"10.1145\/3498667"},{"issue":"1","key":"7_CR11","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1023\/A:1019964114625","volume":"15","author":"C Coquand","year":"2002","unstructured":"Coquand, C.: A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. Higher Order Symbol. Comput. 15(1), 57\u201390 (2002). https:\/\/doi.org\/10.1023\/A:1019964114625","journal-title":"Higher Order Symbol. Comput."},{"issue":"2","key":"7_CR12","doi-asserted-by":"publisher","first-page":"525","DOI":"10.2307\/2586554","volume":"65","author":"P Dybjer","year":"2000","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log. 65(2), 525\u2013549 (2000). https:\/\/doi.org\/10.2307\/2586554","journal-title":"J. Symb. Log."},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Frumin, D., Geuvers, H., Gondelman, L., Weide, N.v.d.: Finite sets in homotopy type theory. In: International Conference on Certified Programs and Proofs (CPP \u201918), pp. 201\u2013214. Association for Computing Machinery (2018). https:\/\/doi.org\/10.1145\/3167085","DOI":"10.1145\/3167085"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0305004119000045","volume":"169","author":"HR Gylterud","year":"2020","unstructured":"Gylterud, H.R.: Multisets in type theory. Math. Proc. Cambridge Philos. Soc. 169(1), 1\u201318 (2020). https:\/\/doi.org\/10.1017\/S0305004119000045","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"issue":"4","key":"7_CR15","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1017\/s0956796898003153","volume":"8","author":"M Hedberg","year":"1998","unstructured":"Hedberg, M.: A coherence theorem for Martin-L\u00f6f\u2019s type theory. J. Funct. Program. 8(4), 413\u2013436 (1998). https:\/\/doi.org\/10.1017\/s0956796898003153","journal-title":"J. Funct. Program."},{"issue":"4","key":"7_CR16","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1017\/S0956796800003713","volume":"10","author":"R Hinze","year":"2000","unstructured":"Hinze, R.: Generalizing generalized tries. J. Funct. Program. 10(4), 327\u2013351 (2000). https:\/\/doi.org\/10.1017\/S0956796800003713","journal-title":"J. Funct. Program."},{"issue":"4","key":"7_CR17","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1017\/s0956796899003500","volume":"9","author":"G Hutton","year":"1999","unstructured":"Hutton, G.: A tutorial on the universality and expressiveness of fold. J. Funct. Program. 9(4), 355\u2013372 (1999). https:\/\/doi.org\/10.1017\/s0956796899003500","journal-title":"J. Funct. Program."},{"key":"7_CR18","unstructured":"Jech, T.: The Axiom of Choice. North-Holland (1973)"},{"key":"7_CR19","doi-asserted-by":"publisher","unstructured":"Joram, P., Veltri, N.: Constructive final semantics of finite bags. In: Naumowicz, A., Thiemann, R. (eds.) Interactive Theorem Proving (ITP \u201923). Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, pp. 20:1\u201320:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.20","DOI":"10.4230\/LIPIcs.ITP.2023.20"},{"key":"7_CR20","unstructured":"Lawvere, F.W.: Display of graphics and their applications, as exemplified by 2-categories and the Hegelian \u201ctaco\". In: Proceedings of the First International Conference on Algebraic Methodology and Software Technology, pp. 51\u201374 (1989)"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"McBride, C.: How to keep your neighbours in order. In: Jeuring, J., Chakravarty, M.M.T. (eds.) International conference on Functional programming (ICFP \u201914), pp. 297\u2013309. Association for Computing Machinery (2014). https:\/\/doi.org\/10.1145\/2628136.2628163","DOI":"10.1145\/2628136.2628163"},{"key":"7_CR22","unstructured":"Nordvall Forsberg, F.: Inductive-inductive definitions. Ph.D. thesis, Swansea University (2013)"},{"key":"7_CR23","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)"},{"key":"7_CR24","unstructured":"Piceghello, S.: Coherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theory. Ph.D. thesis, The University of Bergen (2021)"},{"issue":"2","key":"7_CR25","doi-asserted-by":"publisher","first-page":"438","DOI":"10.2307\/2275540","volume":"62","author":"D Pincus","year":"1997","unstructured":"Pincus, D.: The dense linear ordering principle. J. Symb. Log. 62(2), 438\u2013456 (1997). https:\/\/doi.org\/10.2307\/2275540","journal-title":"J. Symb. Log."},{"issue":"2","key":"7_CR26","first-page":"265","volume":"3","author":"L Poinsot","year":"2010","unstructured":"Poinsot, L., Duchamp, G., Tollu, C.: Partial monoids: associativity and confluence. J. Pure Appl. Math. Adv. Appl. 3(2), 265\u2013285 (2010)","journal-title":"J. Pure Appl. Math. Adv. Appl."},{"key":"7_CR27","unstructured":"Streicher, T.: Investigations into intensional type theory. Habilitation thesis (1993)"},{"key":"7_CR28","unstructured":"Swan, A.: If every set has some irreflexive, extensional order, then excluded middle follows. Agda formalisation by Tom De Jong available at https:\/\/www.cs.bham.ac.uk\/~mhe\/TypeTopology\/Ordinals.WellOrderingTaboo.html"},{"issue":"1","key":"7_CR29","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0021-8693(68)90036-7","volume":"8","author":"F Ulmer","year":"1968","unstructured":"Ulmer, F.: Properties of dense and relative adjoint functors. J. Algebra 8(1), 77\u201395 (1968). https:\/\/doi.org\/10.1016\/0021-8693(68)90036-7","journal-title":"J. Algebra"},{"key":"7_CR30","unstructured":"The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013). https:\/\/homotopytypetheory.org\/book\/"},{"key":"7_CR31","doi-asserted-by":"publisher","unstructured":"Watters, S., Nordvall Forsberg, F., Kupke, C.: Agda formalisation of \u201cA Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists\u201d. https:\/\/doi.org\/10.5281\/zenodo.8357335 (2023)","DOI":"10.5281\/zenodo.8357335"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-99-8311-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T07:03:11Z","timestamp":1700636591000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-99-8311-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9789819983100","9789819983117"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-981-99-8311-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}