{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T09:32:12Z","timestamp":1730280732420,"version":"3.28.0"},"reference-count":19,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,6,29]]},"DOI":"10.1109\/lics52264.2021.9470541","type":"proceedings-article","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T20:14:07Z","timestamp":1625688847000},"page":"1-13","source":"Crossref","is-referenced-by-count":0,"title":["Types Are Internal \u221e-Groupoids"],"prefix":"10.1109","author":[{"given":"Eric","family":"Finster","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antoine","family":"Allioux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","article-title":"Two-level type theory and applications","volume":"abs 1705 3307","author":"annenkov","year":"2017","journal-title":"CoRR"},{"year":"2020","key":"ref11","article-title":"Agda 2.6.1.1 documentation"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0049-237X(08)71945-1","article-title":"An intuitionistic theory of types: Predicative part","volume":"80","author":"martin-l\u00f6f","year":"1975","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"journal-title":"Homotopy Type Theory Univalent Foundations of Mathematics","year":"2013","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681500009X"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"ref16","article-title":"Dependency pairs termination in dependent type theory modulo rewriting","volume":"abs 1906 11649","author":"blanqui","year":"2019","journal-title":"CoRR"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000486"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525896"},{"key":"ref19","article-title":"Types are internal ?-groupoids (extended version)","author":"allioux","year":"2021","journal-title":"ArXiv Preprint"},{"key":"ref4","article-title":"?-operads as analytic monads","author":"gepner","year":"2017","journal-title":"arXiv preprint arXiv 1712 06469"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2010.02.012"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"article-title":"The Taming of the Rew: A Type Theory with Computational Assumptions","year":"0","author":"cockx","key":"ref5"},{"key":"ref8","article-title":"A type theory for synthetic ?-categories","author":"riehl","year":"2017","journal-title":"arXiv preprint arXiv 1705 07442"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1006\/aima.1997.1695"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004112000394"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.09.012"}],"event":{"name":"2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","start":{"date-parts":[[2021,6,29]]},"location":"Rome, Italy","end":{"date-parts":[[2021,7,2]]}},"container-title":["2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9470497\/9470501\/09470541.pdf?arnumber=9470541","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T15:46:21Z","timestamp":1652197581000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9470541\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,29]]},"references-count":19,"URL":"https:\/\/doi.org\/10.1109\/lics52264.2021.9470541","relation":{},"subject":[],"published":{"date-parts":[[2021,6,29]]}}}