{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:07:01Z","timestamp":1784200021509,"version":"3.55.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-23-1-0760"],"award-info":[{"award-number":["FA9550-23-1-0760"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100032827","name":"Advanced Research and Invention Agency","doi-asserted-by":"crossref","award":["Programme on Safeguarded AI"],"award-info":[{"award-number":["Programme on Safeguarded AI"]}],"id":[{"id":"10.13039\/100032827","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["Consolidator Grant BLAST"],"award-info":[{"award-number":["Consolidator Grant BLAST"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n                    We present Dependent Lambek Calculus (Lambek\n                    <jats:sup>\n                      <jats:monospace>D<\/jats:monospace>\n                    <\/jats:sup>\n                    ), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek\n                    <jats:sup>\n                      <jats:monospace>D<\/jats:monospace>\n                    <\/jats:sup>\n                    , linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.\n                  <\/jats:p>\n                  <jats:p>\n                    We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek\n                    <jats:sup>\n                      <jats:monospace>D<\/jats:monospace>\n                    <\/jats:sup>\n                    using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.\n                  <\/jats:p>","DOI":"10.1145\/3729281","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"773-796","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-1258-9501","authenticated-orcid":false,"given":"Steven","family":"Schaefer","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3031-4930","authenticated-orcid":false,"given":"Nathan","family":"Varner","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8338-8973","authenticated-orcid":false,"given":"Pedro Henrique","family":"Azevedo de Amorim","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8141-195X","authenticated-orcid":false,"given":"Max S.","family":"New","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681500009X"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs Terms and Models (CSL 1994). doi:10.1007\/BFb0022251","DOI":"10.1007\/BFb0022251"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-3598-8_12"},{"key":"e_1_3_2_5_1","unstructured":"Noam Chomsky. 1963. Formal Properties of Grammars. Handbook of Mathematical Psychology II (1963) 323\u2013418. Retrieved April 9 2025 from https:\/\/archive.org\/details\/handbookofmathem017893mbp\/page\/322\/mode\/2up"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000232"},{"key":"e_1_3_2_7_1","unstructured":"Thierry Coquand. 2013. Presheaf model of type theory. (2013). Retrieved April 8 2025 from https:\/\/www.cse.chalmers.se\/~coquand\/presheaf.pdf"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","unstructured":"Nils Anders Danielsson. 2010. Total Parser Combinators. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (Baltimore Maryland USA) (ICFP \u201910). 285\u2013296. doi:10.1145\/1863543.1863585","DOI":"10.1145\/1863543.1863585"},{"key":"e_1_3_2_9_1","unstructured":"Brian John Day. 1970. Construction of biclosed categories. Ph.D. Dissertation. University of New South Wales PhD thesis. Retrieved April 8 2025 from https:\/\/web.science.mq.edu.au\/~street\/DayPhD.pdf"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","unstructured":"Romain Edelmann Jad Hamza and Viktor Kun\u010dak. 2020. Zippy LL(1) parsing with derivatives. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (Online) (PLDI 2020). doi:10.1145\/3385412.3385992","DOI":"10.1145\/3385412.3385992"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473583"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Alain Frisch and Luca Cardelli. 2004. Greedy Regular Expression Matching. In Automata Languages and Programming (Turku Finland) (ICALP 2004). doi:10.1007\/978-3-540-27836-8_53","DOI":"10.1007\/978-3-540-27836-8_53"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","unstructured":"Nicola Gambino and Martin Hyland. 2003. Wellfounded Trees and Dependent Polynomial Functors. In Types for Proofs and Programs (Torino Italy) (TYPES 2003). 210\u2013225. doi:10.1007\/978-3-540-24849-1_14","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","unstructured":"Maxime Guillaume Sylvain Pogodalla and Vincent Tourneur. 2024. ACGtk: A Toolkit for Developing and Running Abstract Categorial Grammars. In Functional and Logic Programming (Kumamoto Japan) (17th International Symposium FLOPS 2024). 13\u201330. doi:10.1007\/978-981-97-2300-3_2","DOI":"10.1007\/978-981-97-2300-3_2"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","unstructured":"Fritz Henglein and Lasse Nielsen. 2011. Regular expression containment: coinductive axiomatization and computational interpretation. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Austin Texas USA) (POPL \u201911). 385\u2013398. doi:10.1145\/1926385.1926429","DOI":"10.1145\/1926385.1926429"},{"key":"e_1_3_2_18_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. Cambridge University Press 79\u2013130.","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","unstructured":"Jacques-Henri Jourdan Franccois Pottier and Xavier Leroy. 2012. Validating LR(1) Parsers. In Programming Languages and Systems 21st European Symposium on Programming (Tallinn Estonia) (ESOP 2012). 397\u2013416. doi:10.1007\/978-3-642-28869-2_20","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Nara Japan) (ICFP 2016). 256\u2013269. doi:10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Neelakantan R. Krishnaswami Pierre Pradic and Nick Benton. 2015. Integrating Linear and Dependent Types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai India) (POPL \u201915). 17\u201330. doi:10.1145\/2676726.2676969","DOI":"10.1145\/2676726.2676969"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1958.11989160"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"J. Lambek. 1988. Categorial and Categorical Grammars. 297\u2013317. doi:10.1007\/978-94-015-6878-4_11","DOI":"10.1007\/978-94-015-6878-4_11"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","unstructured":"Sam Lasser Chris Casinghino Kathleen Fisher and Cody Roux. 2021. CoStar: A Verified ALL(*) Parser. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Online) (PLDI 2021). 420\u2013434. doi:10.1145\/3453483.3454053","DOI":"10.1145\/3453483.3454053"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","unstructured":"Haas Lei\u00df. 1992. Towards Kleene Algebra with recursion (CSL 1991). doi:10.1007\/BFb0023771","DOI":"10.1007\/BFb0023771"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Zhaohui Luo. 2018. Substructural Calculi with Dependent Types. In Linearity & TLLA Joint Workshop (Oxford UK). doi:10.29007\/qrqp","DOI":"10.29007\/qrqp"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2021.10"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.32.0114"},{"key":"e_1_3_2_30_1","unstructured":"Aarne Ranta. 2011. Grammatical Framework: Programming with Multilingual Grammars. CSLI Publications Stanford. ISBN-10: 1-57586-626-9 (Paper) 1-57586-627-7 (Cloth)."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"J.C. Reynolds. 2002. Separation logic: a logic for shared mutable data structures. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen Denmark) (LICS 2002). 55\u201374. doi:10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","unstructured":"Steven Schaefer Nathan Varner Pedro Henrique Azevedo de Amorim and Max S. New. 2025a. Agda Formalization of \u201cIntrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus\u201d. doi:10.5281\/zenodo.15243560","DOI":"10.5281\/zenodo.15243560"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","unstructured":"Steven Schaefer Nathan Varner Pedro H. Azevedo de Amorim and Max S. New. 2025b. Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus (Extended Version). doi:10.48550\/arXiv.2504.03995 arXiv:2504.03995","DOI":"10.48550\/arXiv.2504.03995"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/092\/1003210"},{"key":"e_1_3_2_35_1","unstructured":"The Agda Community. 2024. Cubical Agda Library. Retrieved April 8 2025 from https:\/\/github.com\/agda\/cubical"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/363347.363387"},{"key":"e_1_3_2_37_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"The Univalent Foundations Program","year":"2013","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. Retrieved April 8, 2025 from https:\/\/homotopytypetheory.org\/book"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","unstructured":"Matthijs V\u00e1k\u00e1r. 2015. A Categorical Semantics for Linear Logical Frameworks. In Foundations of Software Science and Computation Structures (London UK) (FoSSaCS 2015). 102\u2013116. doi:10.1007\/978-3-662-46678-0_7","DOI":"10.1007\/978-3-662-46678-0_7"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and understanding bugs in C compilers. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (San Jose California USA) (PLDI \u201911). 283\u2013294. doi:10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729281","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729281","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:06:31Z","timestamp":1784196391000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729281"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":39,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729281"],"URL":"https:\/\/doi.org\/10.1145\/3729281","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}