{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,12]],"date-time":"2026-04-12T03:10:36Z","timestamp":1775963436590,"version":"3.50.1"},"reference-count":18,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.429.13","type":"journal-article","created":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T19:20:49Z","timestamp":1758568849000},"page":"234-248","source":"Crossref","is-referenced-by-count":1,"title":["ViCAR: Visualizing Categories with Automated Rewriting in Coq"],"prefix":"10.4204","volume":"429","author":[{"given":"Bhakti","family":"Shah","sequence":"first","affiliation":[]},{"given":"Willam","family":"Spencer","sequence":"additional","affiliation":[]},{"given":"Laura","family":"Zielinski","sequence":"additional","affiliation":[]},{"given":"Ben","family":"Caldwell","sequence":"additional","affiliation":[]},{"given":"Adrian","family":"Lehmann","sequence":"additional","affiliation":[]},{"given":"Robert","family":"Rand","sequence":"additional","affiliation":[]}],"member":"2720","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"key":"beylin1996coherence","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/3-540-61780-9_61","article-title":"Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids","volume-title":"Types for Proofs and Programs","author":"Beylin","year":"1996"},{"key":"braibant2011tactics","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-25379-9_14","article-title":"Tactics for reasoning modulo AC in Coq","volume-title":"International Conference on Certified Programs and Proofs","author":"Braibant","year":"2011"},{"key":"chabassier2023graphical","article-title":"A graphical interface for diagrammatic proofs in proof assistants","volume-title":"29th International Conference on Types for Proofs and Programs TYPES 2023\u2013Abstracts","author":"Chabassier","year":"2023"},{"key":"coecke-duncan-zx","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-70583-3_25","article-title":"Interacting Quantum Observables","volume-title":"Automata, Languages and Programming","author":"Coecke","year":"2008"},{"key":"coecke2017picturing","doi-asserted-by":"publisher","DOI":"10.1017\/9781316219317","volume-title":"Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning","author":"Coecke","year":"2017"},{"key":"eilenberg1966closed","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-642-99902-4_22","article-title":"Closed categories","volume-title":"Proceedings of the Conference on Categorical Algebra: La Jolla 1965","author":"Eilenberg","year":"1966"},{"key":"gross2014experience","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-08970-6_18","article-title":"Experience implementing a performant category-theory library in Coq","volume-title":"Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings 5","author":"Gross","year":"2014"},{"key":"hietala2021sqir","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.21","article-title":"Proving Quantum Programs Correct","volume-title":"12th International Conference on Interactive Theorem Proving (ITP 2021)","volume":"193","author":"Hietala","year":"2021"},{"key":"hietala2021voqc","doi-asserted-by":"publisher","DOI":"10.1145\/3434318","article-title":"A Verified Optimizer for Quantum Circuits","volume":"5","author":"Hietala","year":"2021","journal-title":"Proc. ACM Program. Lang."},{"key":"pyzx","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.4204\/EPTCS.318.14","article-title":"PyZX: Large Scale Automated Diagrammatic Reasoning","volume-title":"Proceedings 16th International Conference on Quantum Physics and Logic, Chapman University, Orange, CA, USA., 10-14 June 2019","volume":"318","author":"Kissinger","year":"2020"},{"issue":"4","key":"kissinger2022simulating","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ac5d20","article-title":"Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions","volume":"7","author":"Kissinger","year":"2022","journal-title":"Quantum Science and Technology"},{"key":"lafont2024diagram","article-title":"A diagram editor to mechanise categorical proofs","volume-title":"35es Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2024)","author":"Lafont","year":"2024"},{"issue":"2","key":"magnus79","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1214\/aos\/1176344621","article-title":"The Commutation Matrix: Some Properties and Applications","volume":"7","author":"Magnus","year":"1979","journal-title":"The Annals of Statistics"},{"key":"megacz2007coinductive","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1292597.1292601","article-title":"A coinductive monad for prop-bounded recursion","volume-title":"Proceedings of the 2007 workshop on Programming languages meets program verification","author":"Megacz","year":"2007"},{"key":"paykin2017qwire","series-title":"POPL '17","doi-asserted-by":"publisher","first-page":"846","DOI":"10.1145\/3009837.3009894","article-title":"QWIRE: A Core Language for Quantum Circuits","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages","author":"Paykin","year":"2017"},{"key":"Selinger2010","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-12821-9_4","article-title":"A Survey of Graphical Languages for Monoidal Categories","volume-title":"New Structures for Physics","author":"Selinger","year":"2010"},{"key":"coq-typeclasses","series-title":"TPHOLs '08","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23","article-title":"First-Class Type Classes","volume-title":"Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics","author":"Sozeau","year":"2008"},{"key":"hottbook","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Univalent Foundations Program","year":"2013"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T18:16:40Z","timestamp":1759169800000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2404.08163v2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"references-count":18,"URL":"https:\/\/doi.org\/10.4204\/eptcs.429.13","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]}}}