{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:06Z","timestamp":1775790726560,"version":"3.50.1"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["206263"],"award-info":[{"award-number":["206263"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Fonds de recherche du Qu\u00e9bec - Nature et Technologies","award":["253521"],"award-info":[{"award-number":["253521"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    In this paper, we introduce\n                    <jats:sc>DeLaM<\/jats:sc>\n                    , a dependent layered modal type theory which enables meta-programming in Martin-L\u00f6f type theory (MLTT) with recursion principles on open code.\n                    <jats:sc>DeLaM<\/jats:sc>\n                    includes three layers: the layer of static syntax objects of MLTT without any computation, the layer of pure MLTT with the computational behaviors, and the meta-programming layer, which extends MLTT with support for quoting an open MLTT code object, composing, and analyzing open code using recursion. We can also execute a code object at the meta-programming layer. The expressive power strictly increases as we move up in a given layer. In particular, while code objects only describe static syntax, we allow computation at the MLTT and meta-programming layer. As a result,\n                    <jats:sc>DeLaM<\/jats:sc>\n                    provides a dependently typed foundation for meta-programming that supports both type-safe code generation and code analysis. We prove the weak normalization of\n                    <jats:sc>DeLaM<\/jats:sc>\n                    and the decidability of convertibility using Kripke logical relations.\n                  <\/jats:p>","DOI":"10.1145\/3704851","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"416-445","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A Dependent Type Theory for Meta-programming with Intensional Analysis"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6710-6262","authenticated-orcid":false,"given":"Jason Z. S.","family":"Hu","sequence":"first","affiliation":[{"name":"McGill University, Montr\u00e9al, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2549-4276","authenticated-orcid":false,"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University, Montr\u00e9al, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation Thesis. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen Munich Germany. https:\/\/www.cse.chalmers.se\/~abela\/habil.pdf"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3635800.3636964"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","unstructured":"Thorsten Altenkirch Martin Hofmann and Thomas Streicher. 1995. Categorical Reconstruction of a Reduction Free Normalization Proof. In Proceedings of the 6th International Conference on Category Theory and Computer Science CTCS 1995 Cambridge UK August 7-11 1995 (Lecture Notes in Computer Science Vol. 953) David H. Pitt David E. Rydeheard and Peter T. Johnstone (Eds.). Springer 182\u2013199. https:\/\/doi.org\/10.1007\/3-540-60164-3_27 10.1007\/3-540-60164-3_27","DOI":"10.1007\/3-540-60164-3_27"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2016.6"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:1)2017"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2022.13"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","unstructured":"Mathieu Boespflug and Brigitte Pientka. 2011. Multi-level Contextual Type Theory. In Proceedings of the 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice LFMTP 2011 Nijmegen the Netherlands August 26 2011 (EPTCS Vol. 71) Herman Geuvers and Gopalan Nadathur (Eds.). 29\u201343. https:\/\/doi.org\/10.4204\/EPTCS.71.3 10.4204\/EPTCS.71.3","DOI":"10.4204\/EPTCS.71.3"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103705"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503887.2503889"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000154"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/64805"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_26_1","volume-title":"Foundations and Applications of Modal Type Theories","author":"Hu Jason Z. S.","year":"2024","unstructured":"Jason Z. S. Hu. 2024. Foundations and Applications of Modal Type Theories. PhD Thesis. McGill University, Montr\u00e9al, Canada."},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000060"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2404.17065"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_3"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498700"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236773"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547641"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0012"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785683"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571739"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.TYPES.2022.6"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41582-1_10"},{"key":"e_1_3_2_46_1","unstructured":"Makarius Wenzel et al. 2024. The Isabelle\/Isar Reference Manual. https:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167091"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000118"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704851","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704851","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:45Z","timestamp":1770200145000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704851"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704851"],"URL":"https:\/\/doi.org\/10.1145\/3704851","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}