{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T04:15:23Z","timestamp":1783484123830,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","funder":[{"name":"National Science and Technology Council of Taiwan","award":["NSTC 114-2222-E-001-001-MY3"],"award-info":[{"award-number":["NSTC 114-2222-E-001-001-MY3"]}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/Y000455\/2"],"award-info":[{"award-number":["EP\/Y000455\/2"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779090","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"201-215","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3250-1331","authenticated-orcid":false,"given":"Liang-Ting","family":"Chen","sequence":"first","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6157-9288","authenticated-orcid":false,"given":"Fredrik","family":"Nordvall Forsberg","sequence":"additional","affiliation":[{"name":"University of Strathclyde, Glasgow, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2855-5717","authenticated-orcid":false,"given":"Tzu-Chun","family":"Tsai","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_3_2_2_2_1","unstructured":"Agda issue. 2019. A variant of Cubical Agda that is consistent with UIP. https:\/\/github.com\/agda\/agda\/issues\/3750"},{"key":"e_1_3_2_2_3_1","unstructured":"Agda issue. 2021. Interleaved mutual and equality constructors. https:\/\/github.com\/agda\/agda\/issues\/5362"},{"key":"e_1_3_2_2_4_1","unstructured":"Agda issue. 2022. Fix #5816: skip generating cubical clauses for Prop stuff. https:\/\/github.com\/agda\/agda\/pull\/5897"},{"key":"e_1_3_2_2_5_1","unstructured":"Agda issue. 2025. Implement a \u2013cubical=no-glue option. https:\/\/github.com\/agda\/agda\/pull\/7861"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_7"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:1)2017"},{"key":"e_1_3_2_2_10_1","unstructured":"Thorsten Altenkirch Ambrus Kaposi and Szumi Xie. 2026. The groupoid-syntax of type theory is a set. In Computer Science Logic (CSL\u201926). https:\/\/arxiv.org\/abs\/2509.14988 To appear."},{"key":"e_1_3_2_2_11_1","unstructured":"Thorsten Altenkirch and Conor McBride. 2006. Towards observational type theory. (2006). http:\/\/www.strictlypositive.org\/ott.pdf"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000268"},{"key":"e_1_3_2_2_13_1","unstructured":"Viktor Bense Ambrus Kaposi and Szumi Xie. 2024. Strict syntax of type theory via alpha-normalisation. (2024). https:\/\/vipwww.itu.dk\/research\/types2024\/slides\/Viktor Bense - Strict syntax of type theory via alpha-normalisation.pdf Presented at TYPES\u201924."},{"key":"e_1_3_2_2_14_1","volume-title":"Peter LeFanu Lumsdaine, and Anders M\u00f6rtberg","author":"Brunerie Guillaume","year":"2019","unstructured":"Guillaume Brunerie, Menno de Boer, Peter LeFanu Lumsdaine, and Anders M\u00f6rtberg. 2019. A formalization of the initiality conjecture in Agda. (2019). https:\/\/guillaumebrunerie.github.io\/pdf\/initiality.pdf Slides of a talk at the Homotopy Type Theory 2019 Conference."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17802827"},{"key":"e_1_3_2_2_18_1","unstructured":"Thierry Coquand. 2020. Generalised algebraic presentation of type theory. (2020). https:\/\/www.cse.chalmers.se\/~coquand\/cwf2.pdf"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000356"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000069"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_7"},{"key":"e_1_3_2_2_22_1","volume-title":"A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory. Licentiate thesis. Department of Mathematics","author":"de Boer Menno","unstructured":"Menno de Boer. 2020. A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory. Licentiate thesis. Department of Mathematics, Stockholm University. https:\/\/urn.kb.se\/resolve?urn=urn"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2021.6"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48959-2_11"},{"key":"e_1_3_2_2_26_1","unstructured":"Thomas Ehrhard. 1988. Une s\u00e9mantique cat\u00e9gorique des types d\u00e9pendents. Ph. D. Dissertation. Universit\u00e9 Paris VII."},{"key":"e_1_3_2_2_27_1","unstructured":"Thiago Felicissimo and Nicolas Tabareau. 2025. Towards quotient inductive types in observational type theory. (2025). https:\/\/msp.cis.strath.ac.uk\/types2025\/abstracts\/ TYPES2025_paper85.pdf Presented at TYPES\u201925."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_13"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0963-1"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"e_1_3_2_2_32_1","volume-title":"Type theory in a type theory with quotient inductive types. Ph. D. Dissertation","author":"Kaposi Ambrus","unstructured":"Ambrus Kaposi. 2017. Type theory in a type theory with quotient inductive types. Ph. D. Dissertation. University of Nottingham. https:\/\/eprints.nottingham.ac.uk\/41385\/"},{"key":"e_1_3_2_2_33_1","volume-title":"Re: Separate definition of constructors? Post to the Agda mailing list, https:\/\/web.archive.org\/web\/20241004151846\/https:\/\/lists.chalmers.se\/pipermail\/agda\/2019\/011176.html.","author":"Kaposi Ambrus","year":"2019","unstructured":"Ambrus Kaposi. 2019. Re: Separate definition of constructors? Post to the Agda mailing list, https:\/\/web.archive.org\/web\/20241004151846\/https:\/\/lists.chalmers.se\/pipermail\/agda\/2019\/011176.html."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:10)2020"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747535"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000307"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394770"},{"key":"e_1_3_2_2_39_1","unstructured":"Am\u00e9lia Liao Daniel S\u00f6lch Na\u00efm Favier and Reed Mullanix. 2022. Displayed categories. https:\/\/1lab.dev\/Cat.Displayed.Base.html."},{"key":"e_1_3_2_2_40_1","volume-title":"Running circles around (in) your proof assistant","author":"Licata Dan","year":"2011","unstructured":"Dan Licata. 2011. Running circles around (in) your proof assistant; or, quotients that compute. https:\/\/homotopytypetheory.org\/2011\/04\/23\/running-circles- around-in-your-proof-assistant\/"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S030500411900015X"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2754931"},{"key":"e_1_3_2_2_43_1","volume-title":"Dependently Typed Functional Programs and their Proofs. Ph. D. Dissertation","author":"McBride Conor","unstructured":"Conor McBride. 1999. Dependently Typed Functional Programs and their Proofs. Ph. D. Dissertation. University of Edinburgh. https:\/\/era.ed.ac.uk\/bitstream\/id\/600\/ECS-LFCS-00-419.pdf"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863495.1863497"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_2_2_46_1","unstructured":"Lo\u00efc Pujet. 2024. Observational Coq. GitHub repository. https:\/\/github.com\/loic-p\/observational-coq"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571739"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_12"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100061284"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(1:43)2022"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"e_1_3_2_2_53_1","volume-title":"Towards Computational UIP in Cubical Agda. Master\u2019s thesis. Ecole polytechnique","author":"Tan Yee-Jian","unstructured":"Yee-Jian Tan. 2025. Towards Computational UIP in Cubical Agda. Master\u2019s thesis. Ecole polytechnique; Inria - Paris."},{"key":"e_1_3_2_2_54_1","unstructured":"Yee-Jian Tan Andreas Nuyts and Dominique Devriese. 2025. Towards Computational UIP in Cubical Agda. https:\/\/arxiv.org\/abs\/2511.21209"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T03:45:33Z","timestamp":1783482333000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779090"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":55,"alternative-id":["10.1145\/3779031.3779090","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779090","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}