{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,18]],"date-time":"2026-02-18T23:01:19Z","timestamp":1771455679843,"version":"3.50.1"},"reference-count":97,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids \u00e0 la Homotopy Type Theory, and show how to derive an equational theory for it, presented by 2-combinators witnessing equivalences of type isomorphisms.<\/jats:p>\n          <jats:p>We establish a correspondence between the syntactic groupoid of the language and a formally presented univalent subuniverse of finite types. The correspondence relates 1-combinators to 1-paths, and 2-combinators to 2-paths in the universe, which is shown to be sound and complete for both levels, forming an equivalence of groupoids. We use this to establish a Curry-Howard-Lambek correspondence between Reversible Logic, Reversible Programming Languages, and Symmetric Rig Groupoids, by showing that the syntax of Pi is presented by the free symmetric rig groupoid, given by finite sets and bijections.<\/jats:p>\n          <jats:p>Using the formalisation of our results, we perform normalisation-by-evaluation, verification and synthesis of reversible logic gates, motivated by examples from quantum computing. We also show how to reason about and transfer theorems between different representations of reversible circuits.<\/jats:p>","DOI":"10.1145\/3498667","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2030-8056","authenticated-orcid":false,"given":"Vikraman","family":"Choudhury","sequence":"first","affiliation":[{"name":"Indiana University, USA \/ University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8361-2912","authenticated-orcid":false,"given":"Jacek","family":"Karwowski","sequence":"additional","affiliation":[{"name":"University of Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1025-7331","authenticated-orcid":false,"given":"Amr","family":"Sabry","sequence":"additional","affiliation":[{"name":"Indiana University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITCS.2017.23"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11548133_1"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.002"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5281\/ZENODO.2562110"},{"key":"e_1_2_2_5_1","volume-title":"Computational Semantics of CartesianCubical Type Theory. Ph. D. Dissertation","author":"Angiuli Carlo","unstructured":"Carlo Angiuli . 2019. Computational Semantics of CartesianCubical Type Theory. Ph. D. Dissertation . Carnegie Mellon University . Pittsburgh, PA. https:\/\/www.cs.cmu.edu\/~cangiuli\/thesis\/thesis.pdf Carlo Angiuli. 2019. Computational Semantics of CartesianCubical Type Theory. Ph. D. Dissertation. Carnegie Mellon University. Pittsburgh, PA. https:\/\/www.cs.cmu.edu\/~cangiuli\/thesis\/thesis.pdf"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434293"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-56478-9_3"},{"key":"e_1_2_2_8_1","unstructured":"John C. Baez Fabrizio Genovese Jade Master and Michael Shulman. 2021. Categories of Nets. arXiv:2101.04238 [cs math] April arxiv:2101.04238. arxiv:2101.04238  John C. Baez Fabrizio Genovese Jade Master and Michael Shulman. 2021. Categories of Nets. arXiv:2101.04238 [cs math] April arxiv:2101.04238. arxiv:2101.04238"},{"key":"e_1_2_2_9_1","first-page":"66","article-title":"HIGHER DIMENSIONAL ALGEBRA VII: GROUPOIDIFICATION","volume":"24","author":"Baez John C","year":"2010","unstructured":"John C Baez , Alexander E Hoffnung , and Christopher D Walker . 2010 . HIGHER DIMENSIONAL ALGEBRA VII: GROUPOIDIFICATION . Theory and Applications of Categories , 24 (2010), 66 . http:\/\/www.tac.mta.ca\/tac\/volumes\/24\/18\/24-18abs.html John C Baez, Alexander E Hoffnung, and Christopher D Walker. 2010. HIGHER DIMENSIONAL ALGEBRA VII: GROUPOIDIFICATION. Theory and Applications of Categories, 24 (2010), 66. http:\/\/www.tac.mta.ca\/tac\/volumes\/24\/18\/24-18abs.html","journal-title":"Theory and Applications of Categories"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/142137.142162"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0017210"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2011517.2011525"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2010.06.019"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/010"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1038\/scientificamerican0785-48"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.3390\/e21101023"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_61"},{"key":"e_1_2_2_18_1","volume-title":"Bj\u00f8rn Ian Dundas, and Daniel R. Grayson","author":"Bezem Marc","year":"2021","unstructured":"Marc Bezem , Ulrik Buchholtz , Pierre Cagne , Bj\u00f8rn Ian Dundas, and Daniel R. Grayson . 2021 . Symmetry . https:\/\/github.com\/UniMath\/SymmetryBook Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bj\u00f8rn Ian Dundas, and Daniel R. Grayson. 2021. Symmetry. https:\/\/github.com\/UniMath\/SymmetryBook"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(89)90160-6"},{"key":"e_1_2_2_20_1","volume-title":"Dagger Traced Symmetric Monoidal Categories and Reversible Programming. In Workshop on Reversible Computation.","author":"Bowman William J.","year":"2011","unstructured":"William J. Bowman , Roshan P. James , and Amr Sabry . 2011 . Dagger Traced Symmetric Monoidal Categories and Reversible Programming. In Workshop on Reversible Computation. William J. Bowman, Roshan P. James, and Amr Sabry. 2011. Dagger Traced Symmetric Monoidal Categories and Reversible Programming. In Workshop on Reversible Computation."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330081"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209150"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.013"},{"key":"e_1_2_2_24_1","volume-title":"Embracing the Laws of Physics: Three Reversible Models of Computation. Advances in Computers, 126","author":"Carette Jacques","year":"2021","unstructured":"Jacques Carette , Roshan P. James , and Amr Sabry . 2021. Embracing the Laws of Physics: Three Reversible Models of Computation. Advances in Computers, 126 ( 2021 ), arxiv:1811.03678 Jacques Carette, Roshan P. James, and Amr Sabry. 2021. Embracing the Laws of Physics: Three Reversible Models of Computation. Advances in Computers, 126 (2021), arxiv:1811.03678"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_6"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-52482-1_10"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434290"},{"key":"e_1_2_2_28_1","unstructured":"Vikraman Choudhury and Marcelo Fiore. 2019. The Finite-Multiset Construction in HoTT. Aug. 40. https:\/\/hott.github.io\/HoTT-2019\/conf-slides\/Choudhury.pdf  Vikraman Choudhury and Marcelo Fiore. 2019. The Finite-Multiset Construction in HoTT. Aug. 40. https:\/\/hott.github.io\/HoTT-2019\/conf-slides\/Choudhury.pdf"},{"key":"e_1_2_2_29_1","unstructured":"Vikraman Choudhury and Marcelo Fiore. 2021. Free Commutative Monoids in Homotopy Type Theory. Oct. arxiv:2110.05412v1  Vikraman Choudhury and Marcelo Fiore. 2021. Free Commutative Monoids in Homotopy Type Theory. Oct. arxiv:2110.05412v1"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5671746"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"Vikraman Choudhury Jacek Karwowski and Amr Sabry. 2021. Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages. Oct. arxiv:2110.05404v1  Vikraman Choudhury Jacek Karwowski and Amr Sabry. 2021. Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages. Oct. arxiv:2110.05404v1","DOI":"10.1145\/3498667"},{"key":"e_1_2_2_32_1","unstructured":"Dan Christensen. 2015. A Characterization of Univalent Fibrations. June 53. http:\/\/sweet.ua.pt\/dirk\/ct2015\/slides\/Christensen.pdf  Dan Christensen. 2015. A Characterization of Univalent Fibrations. June 53. http:\/\/sweet.ua.pt\/dirk\/ct2015\/slides\/Christensen.pdf"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2015.5"},{"key":"e_1_2_2_34_1","unstructured":"Jonathan Asher Cohen. 2009. Coherence for Rewriting 2-Theories. arXiv:0904.0125 [cs math] April arxiv:0904.0125. arxiv:0904.0125  Jonathan Asher Cohen. 2009. Coherence for Rewriting 2-Theories. arXiv:0904.0125 [cs math] April arxiv:0904.0125. arxiv:0904.0125"},{"key":"e_1_2_2_35_1","volume-title":"Lambda Calculus","author":"To","unstructured":"1980. To H.B. Curry: Essays on Combinatory Logic , Lambda Calculus , and Formalism, Haskell B. Curry, J. Roger Hindley, and J. P. Seldin (Eds.). Academic Press , London ; New York. isbn:978-0-12-349050-6 lccn:QA9.2 .T6 1980. To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Haskell B. Curry, J. Roger Hindley, and J. P. Seldin (Eds.). Academic Press, London ; New York. isbn:978-0-12-349050-6 lccn:QA9.2 .T6"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_19"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005391"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-018-0459-1"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2021.106738"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02650179"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/jdm096"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15155-2_33"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664576"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2018.15"},{"key":"e_1_2_2_45_1","volume-title":"Reversibility for Efficient Computing. Ph. D. Dissertation","author":"Frank Michael P.","unstructured":"Michael P. Frank . 1999. Reversibility for Efficient Computing. Ph. D. Dissertation . Massachusetts Institute of Technology . USA. Michael P. Frank. 1999. Reversibility for Efficient Computing. Ph. D. Dissertation. Massachusetts Institute of Technology. USA."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01857727"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2013.06.028"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004119000045"},{"key":"e_1_2_2_49_1","volume-title":"Anthony J. G. Hey (Ed.)","unstructured":"1999. Feynman and Computation: Exploring the Limits of Computers , Anthony J. G. Hey (Ed.) . Perseus Books , USA. isbn:978-0-7382-0057-6 1999. Feynman and Computation: Exploring the Limits of Computers, Anthony J. G. Hey (Ed.). Perseus Books, USA. isbn:978-0-7382-0057-6"},{"key":"e_1_2_2_50_1","unstructured":"Florent Hiver. 2021. Coq-Combi: The Coxeter Presentation of the Symmetric Group. Mathematical Components. https:\/\/github.com\/math-comp\/Coq-Combi\/blob\/1ba924ecc1a1c7714a9b3a2dbb23d91af2a1193a\/theories\/SymGroup\/presentSn.v  Florent Hiver. 2021. Coq-Combi: The Coxeter Presentation of the Symmetric Group. Mathematical Components. https:\/\/github.com\/math-comp\/Coq-Combi\/blob\/1ba924ecc1a1c7714a9b3a2dbb23d91af2a1193a\/theories\/SymGroup\/presentSn.v"},{"key":"e_1_2_2_51_1","volume-title":"A Logically Reversible Evaluator for the Call-by-Name Lambda Calculus. InterJournal Complex Systems, 46","author":"Huelsbergen Lorenz","year":"1996","unstructured":"Lorenz Huelsbergen . 1996. A Logically Reversible Evaluator for the Call-by-Name Lambda Calculus. InterJournal Complex Systems, 46 ( 1996 ). Lorenz Huelsbergen. 1996. A Logically Reversible Evaluator for the Call-by-Name Lambda Calculus. InterJournal Complex Systems, 46 (1996)."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000377"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.09.004"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103667"},{"key":"e_1_2_2_56_1","volume-title":"James and Amr Sabry","author":"Roshan","year":"2014","unstructured":"Roshan P. James and Amr Sabry . 2014 . Theseus : A High-Level Language for Reversible Computation. In Reversible Computation . Roshan P. James and Amr Sabry. 2014. Theseus: A High-Level Language for Reversible Computation. In Reversible Computation."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1993.1055"},{"key":"e_1_2_2_58_1","volume-title":"Peter LeFanu Lumsdaine, and Vladimir Voevodsky","author":"Kapulkin Chris","year":"2012","unstructured":"Chris Kapulkin , Peter LeFanu Lumsdaine, and Vladimir Voevodsky . 2012 . Univalence in Simplicial Sets . March, arxiv:1203.2553v1 Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. 2012. Univalence in Simplicial Sets. March, arxiv:1203.2553v1"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS\/1050"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0063106"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722298_6"},{"key":"e_1_2_2_62_1","volume-title":"The Art of Computer Programming","author":"Knuth Donald Ervin","year":"1997","unstructured":"Donald Ervin Knuth . 1997. The Art of Computer Programming ( 3 rd ed ed.). Addison-Wesley, Reading , Mass . isbn:978-0-201-89683-1 978-0-201-89684-8 978-0-201-89685-5 lccn:QA76.6 .K64 1997 Donald Ervin Knuth. 1997. The Art of Computer Programming (3rd ed ed.). Addison-Wesley, Reading, Mass. isbn:978-0-201-89683-1 978-0-201-89684-8 978-0-201-89685-5 lccn:QA76.6 .K64 1997","edition":"3"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394800"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_32"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(03)00069-0"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.24033\/bsmf.378"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.53.0183"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059555"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.50.5.869"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/010\/0113289"},{"key":"e_1_2_2_72_1","volume-title":"Natural Associativity and Commutativity","author":"MacLane Saunders","year":"1963","unstructured":"Saunders MacLane . 1963. Natural Associativity and Commutativity . Rice Institute Pamphlet - Rice University Studies , 49, 4 ( 1963 ), Oct., https:\/\/scholarship.rice.edu\/handle\/1911\/62865 Saunders MacLane. 1963. Natural Associativity and Commutativity. Rice Institute Pamphlet - Rice University Studies, 49, 4 (1963), Oct., https:\/\/scholarship.rice.edu\/handle\/1911\/62865"},{"key":"e_1_2_2_73_1","unstructured":"Dmitri Maslov. 2003. Reversible Logic Synthesis.  Dmitri Maslov. 2003. Reversible Logic Synthesis."},{"key":"e_1_2_2_74_1","first-page":"3419","article-title":"G\u00e9n\u00e9rateurs et Relations Des Groupes de Weyl G\u00e9n\u00e9ralis\u00e9s","volume":"258","author":"Matsumoto Hideya","year":"1964","unstructured":"Hideya Matsumoto . 1964 . G\u00e9n\u00e9rateurs et Relations Des Groupes de Weyl G\u00e9n\u00e9ralis\u00e9s . COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES , 258 , 13 (1964), 3419 . Hideya Matsumoto. 1964. G\u00e9n\u00e9rateurs et Relations Des Groupes de Weyl G\u00e9n\u00e9ralis\u00e9s. COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES, 258, 13 (1964), 3419.","journal-title":"COMPTES RENDUS HEBDOMADAIRES DES SEANCES DE L ACADEMIE DES SCIENCES"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785830"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775915"},{"key":"e_1_2_2_77_1","volume-title":"Cubical Agda: Simple Application of Fin: Lehmer Codes. Agda Github Community. https:\/\/github.com\/agda\/cubical\/blob\/a1d2bb38c0794f3cb00610cd6061cf9b5410518d\/Cubical\/Data\/Fin\/LehmerCode.agda","author":"Molzer Martin","year":"2021","unstructured":"Martin Molzer . 2021 . Cubical Agda: Simple Application of Fin: Lehmer Codes. Agda Github Community. https:\/\/github.com\/agda\/cubical\/blob\/a1d2bb38c0794f3cb00610cd6061cf9b5410518d\/Cubical\/Data\/Fin\/LehmerCode.agda Martin Molzer. 2021. Cubical Agda: Simple Application of Fin: Lehmer Codes. Agda Github Community. https:\/\/github.com\/agda\/cubical\/blob\/a1d2bb38c0794f3cb00610cd6061cf9b5410518d\/Cubical\/Data\/Fin\/LehmerCode.agda"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_16"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2017.6"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.32.3266"},{"key":"e_1_2_2_81_1","unstructured":"I. Petrakis. 2019. Univalent Typoids. https:\/\/www.math.lmu.de\/~petrakis\/Typoids.pdf  I. Petrakis. 2019. Univalent Typoids. https:\/\/www.math.lmu.de\/~petrakis\/Typoids.pdf"},{"key":"e_1_2_2_82_1","unstructured":"Stefano Piceghello. 2019. Coherence for Symmetric Monoidal Groupoids in HoTT\/UF. 2. http:\/\/www.ii.uib.no\/~bezem\/abstracts\/TYPES_2019_paper_10  Stefano Piceghello. 2019. Coherence for Symmetric Monoidal Groupoids in HoTT\/UF. 2. http:\/\/www.ii.uib.no\/~bezem\/abstracts\/TYPES_2019_paper_10"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2019.8"},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5620828"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2003.811448"},{"key":"e_1_2_2_86_1","unstructured":"Zachary Sparks and Amr Sabry. 2014. Superstructural Reversible Logic. 12. https:\/\/legacy.cs.indiana.edu\/~sabry\/papers\/reversible-logic.pdf  Zachary Sparks and Amr Sabry. 2014. Superstructural Reversible Logic. 12. https:\/\/legacy.cs.indiana.edu\/~sabry\/papers\/reversible-logic.pdf"},{"key":"e_1_2_2_87_1","unstructured":"Arnaud Spiwack and Thierry Coquand. 2010. Constructively Finite? Universidad de La Rioja. isbn:978-84-96487-50-5 https:\/\/hal.inria.fr\/inria-00503917  Arnaud Spiwack and Thierry Coquand. 2010. Constructively Finite? Universidad de La Rioja. isbn:978-84-96487-50-5 https:\/\/hal.inria.fr\/inria-00503917"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3429979"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10003-2_104"},{"key":"e_1_2_2_90_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations Program","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program . 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations Program , Institute for Advanced Study . https:\/\/homotopytypetheory.org\/book The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Univalent Foundations Program, Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book"},{"key":"e_1_2_2_91_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.dam.2011.05.012"},{"key":"e_1_2_2_92_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703432165"},{"key":"e_1_2_2_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_2_2_94_1","first-page":"255","article-title":"The syntax of coherence","volume":"41","author":"Yanofsky Noson S.","year":"2000","unstructured":"Noson S. Yanofsky . 2000 . The syntax of coherence . Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques , 41 , 4 (2000), 255 \u2013 304 . http:\/\/www.numdam.org\/item\/?id=CTGDC_2000__41_4_255_0 Noson S. Yanofsky. 2000. The syntax of coherence. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques, 41, 4 (2000), 255\u2013304. http:\/\/www.numdam.org\/item\/?id=CTGDC_2000__41_4_255_0","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"e_1_2_2_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/1366230.1366239"},{"key":"e_1_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/1244381.1244404"},{"key":"e_1_2_2_97_1","unstructured":"Brent Abraham Yorgey. 2014. Combinatorial Species and Labelled Structures. Dissertations available from ProQuest Jan. 1\u2013206. https:\/\/repository.upenn.edu\/dissertations\/AAI3668177  Brent Abraham Yorgey. 2014. Combinatorial Species and Labelled Structures. Dissertations available from ProQuest Jan. 1\u2013206. https:\/\/repository.upenn.edu\/dissertations\/AAI3668177"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498667","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:27Z","timestamp":1750188627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":97,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498667"],"URL":"https:\/\/doi.org\/10.1145\/3498667","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}