{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T12:21:17Z","timestamp":1761999677382,"version":"build-2065373602"},"reference-count":52,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1109\/lics.2017.8005147","type":"proceedings-article","created":{"date-parts":[[2017,8,10]],"date-time":"2017-08-10T16:43:24Z","timestamp":1502383404000},"page":"1-12","source":"Crossref","is-referenced-by-count":9,"title":["Data structures for quasistrict higher categories"],"prefix":"10.1109","author":[{"given":"Krzysztof","family":"Bar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jamie","family":"Vicary","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","article-title":"Computing critical pairs in polygraphs","author":"mimram","year":"2009","journal-title":"2009 paper presented at CAMCAD"},{"key":"ref38","article-title":"Implementing polygraphs","author":"mimram","year":"0","journal-title":"presentation at CATHRE ANR meeting"},{"key":"ref33","first-page":"1","article-title":"Globular: a proof assistant for higher-dimensional rewriting","volume":"52","author":"bar","year":"2016","journal-title":"Proc FSCD 2016"},{"journal-title":"Homotopy types of strict 3-groupoids","year":"1998","author":"simpson","key":"ref32"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1998.1724"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1996.0052"},{"journal-title":"Unimath Univalent Mathematics","year":"2016","author":"ahrens","key":"ref37"},{"journal-title":"The HoTT library A formalization of homotopy type theory in Coq","year":"0","author":"bauer","key":"ref36"},{"journal-title":"Data structures for quasistrict higher categories","year":"2016","author":"bar","key":"ref35"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2015.09.011"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061280"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-7954(96)80019-2"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-339050-9.50011-0"},{"key":"ref2","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1017\/S0305004108001783","article-title":"Homotopy theoretic models of identity types","volume":"146","author":"awodey","year":"2008","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"journal-title":"Homotopy Type Theory Univalent Foundations of Mathematics","year":"2013","key":"ref1"},{"key":"ref20","first-page":"2","article-title":"On braidings, syllepses and symmetries","volume":"xli","author":"crans","year":"1998","journal-title":"Cahiers de Topologie et Geometrie Differentiel"},{"key":"ref22","article-title":"Surface diagrams","author":"trimble","year":"1995","journal-title":"nLab Surface diagrams"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525896"},{"journal-title":"Gray categories with duals and their diagrams","year":"2012","author":"barrett","key":"ref24"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(91)90003-P"},{"key":"ref26","article-title":"A survey of graphical languages for monoidal categories","author":"selinger","year":"2009","journal-title":"New Structures for Physics"},{"journal-title":"Low-dimensional Topology and Higher-order Categories","year":"1995","author":"street","key":"ref25"},{"key":"ref50","article-title":"The Opetopic! proof assistant","author":"finster","year":"0","journal-title":"opetopic net"},{"key":"ref51","article-title":"Coinductive definitions","author":"shulman","year":"2011","journal-title":"post at the n-Cat-egory Cafe"},{"journal-title":"Letter to Michael Hopkins","year":"0","author":"breen","key":"ref52"},{"journal-title":"Pursuing stacks","year":"1983","author":"grothendieck","key":"ref10"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003462"},{"key":"ref40","first-page":"12","article-title":"A tensor product for Gray-categories","volume":"5","author":"crans","year":"1999","journal-title":"TAC"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.4310\/HHA.2003.v5.n2.a5"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(2:1)2014"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62950-5_73"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2012.05.010"},{"journal-title":"Biunitary constructions in quantum information","year":"2016","author":"reutter","key":"ref16"},{"journal-title":"Holographic software for quantum networks","year":"2016","author":"jaffe","key":"ref17"},{"key":"ref18","article-title":"Strict 2-category","author":"authors","year":"0","journal-title":"entry on the nLab"},{"journal-title":"Internal bicategories","year":"2012","author":"douglas","key":"ref19"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316071"},{"journal-title":"A very short note on the homotopy ?-calculus","year":"2006","author":"voevodsky","key":"ref3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1063\/1.531236"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.4310\/CDM.2008.v2008.n1.a3"},{"journal-title":"The Classification of Two-dimensional Extended Topological Field Theories","year":"2009","author":"schommer-pries","key":"ref8"},{"key":"ref7","first-page":"12","article-title":"Topological quantumfield theories","author":"atiyah","year":"2009","journal-title":"Geometric and Physics of Knots"},{"key":"ref49","article-title":"Type theory and the opetopes","author":"finster","year":"2012","journal-title":"talk presented at the Polish Seminar on Category Theory and its Applications"},{"key":"ref9","doi-asserted-by":"crossref","DOI":"10.1515\/9781400830558","author":"lurie","year":"2009","journal-title":"Higher Topos Theory (AM-170)"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/s10485-008-9137-4"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2010.01.022"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2010.02.012"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1997.1695"},{"key":"ref42","first-page":"857","article-title":"Multitensors as monads on categories of enriched graphs","volume":"28","author":"weber","year":"2013","journal-title":"TAC"},{"key":"ref41","first-page":"387","article-title":"A cocategorical obstruction to tensor products of gray-categories","volume":"30","author":"bourke","year":"2015","journal-title":"TAC"},{"key":"ref44","first-page":"24","article-title":"Free products of higher operad algebras","volume":"28","author":"weber","year":"2013","journal-title":"TAC"},{"key":"ref43","first-page":"804","article-title":"Multitensor lifting and strictly unital higher category theory","volume":"28","author":"batanin","year":"2013","journal-title":"TAC"}],"event":{"name":"2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","start":{"date-parts":[[2017,6,20]]},"location":"Reykjavik, Iceland","end":{"date-parts":[[2017,6,23]]}},"container-title":["2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7999337\/8005055\/08005147.pdf?arnumber=8005147","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T03:39:00Z","timestamp":1569987540000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8005147\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6]]},"references-count":52,"URL":"https:\/\/doi.org\/10.1109\/lics.2017.8005147","relation":{},"subject":[],"published":{"date-parts":[[2017,6]]}}}