{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T17:08:32Z","timestamp":1785431312697,"version":"3.56.0"},"reference-count":18,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"unspecified","delay-in-days":137,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2026]]},"abstract":"Abstract<\/jats:title>\n \n Traditional category theory is typically based on set-theoretic principles and ideas, which are often nonconstructive. An alternative approach to formalizing category theory is to use\n e<\/jats:sc>\n -category theory, where hom sets become setoids. Our work reconsiders a third approach \u2013\n p<\/jats:sc>\n -category theory \u2013 from \u010cubri\u0107 et al. (\n Mathematical Structures in Computer Science<\/jats:italic>\n 8(2) 153\u2013192, 1998) emphasizing a computational standpoint. We formalize in Rocq a modest library of\n p<\/jats:sc>\n -category theory \u2013 where homs become subsetoids \u2013 and apply it to formalizing algorithms for normalization by evaluation, which are purely categorical but, surprisingly, do not use neutral and normal terms. \u010cubri\u0107 et al. (\n Mathematical Structures in Computer Science<\/jats:italic>\n 8(2) 153\u2013192, 1998) establish only a soundness correctness property by categorical means; here, we extend their work by providing a categorical proof also for a strong completeness property. For this, we formalize the full universal property of the free Cartesian-closed category, which is not known to have been performed before. We further formalize a novel universal property of unquotiented simply typed\n \n \n \n $\\lambda$<\/jats:tex-math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -calculus syntax and apply this to a proof of correctness of a categorical normalization by evaluation algorithm. We pair the overall mathematical development with a formalization in the Rocq proof assistant, following the principle that the formalization exists for practical computation. Indeed, it permits extraction of synthesized normalization programs that compute (long)\n \n \n \n $\\beta$<\/jats:tex-math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n \n \n \n $\\eta$<\/jats:tex-math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -normal forms of simply typed\n \n \n \n $\\lambda$<\/jats:tex-math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -terms together with a derivation of\n \n \n \n $\\beta$<\/jats:tex-math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n \n \n \n $\\eta$<\/jats:tex-math>\n <\/jats:alternatives>\n <\/jats:inline-formula>\n -conversion.\n <\/jats:p>","DOI":"10.1017\/s0960129525100406","type":"journal-article","created":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T11:22:16Z","timestamp":1779103336000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Formal\n p<\/scp>\n -category theory and normalization by evaluation in Rocq"],"prefix":"10.1017","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3595-538X","authenticated-orcid":false,"given":"David","family":"Berry","sequence":"first","affiliation":[{"id":[{"id":"https:\/\/ror.org\/013meh722","id-type":"ROR","asserted-by":"publisher"}],"name":"University of Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8558-3492","authenticated-orcid":false,"given":"Marcelo","family":"Fiore","sequence":"additional","affiliation":[{"id":[{"id":"https:\/\/ror.org\/013meh722","id-type":"ROR","asserted-by":"publisher"}],"name":"University of Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"S0960129525100406_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000263"},{"key":"S0960129525100406_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439922"},{"key":"S0960129525100406_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_18"},{"key":"S0960129525100406_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"S0960129525100406_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002508"},{"key":"S0960129525100406_ref16","volume-title":"A machine-checked correctness proof of Normalization by evaluation for simply typed lambda calculus","author":"Kov\u00e1cs","year":"2017"},{"key":"S0960129525100406_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964007"},{"key":"S0960129525100406_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"S0960129525100406_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"S0960129525100406_ref14","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/5641.003.0015"},{"key":"S0960129525100406_ref17","first-page":"367","volume-title":"Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020","year":"2020"},{"key":"S0960129525100406_ref10","doi-asserted-by":"publisher","DOI":"10.2307\/2268484"},{"key":"S0960129525100406_ref6","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"S0960129525100406_ref8","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"S0960129525100406_ref18","unstructured":"Salvesen, A. and Smith, J. M. (1988). Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988). In: Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science, Washington: IEEE Computer Society Press, 384\u2013391."},{"key":"S0960129525100406_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018615"},{"key":"S0960129525100406_ref1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932506"},{"key":"S0960129525100406_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511863196.005"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129525100406","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T11:22:20Z","timestamp":1779103340000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129525100406\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"references-count":18,"alternative-id":["S0960129525100406"],"URL":"https:\/\/doi.org\/10.1017\/s0960129525100406","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"\u00a9 The Author(s), 2026. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}],"article-number":"e18"}}