{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:01:27Z","timestamp":1770274887622,"version":"3.49.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"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"}]},{"DOI":"10.13039\/501100003151","name":"Fonds de recherche du Qu\u00e9bec \u2013 Nature et technologies","doi-asserted-by":"publisher","award":["253521"],"award-info":[{"award-number":["253521"]}],"id":[{"id":"10.13039\/501100003151","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003151","name":"Fonds de recherche du Qu\u00e9bec \u2013 Nature et technologies","doi-asserted-by":"publisher","award":["304215"],"award-info":[{"award-number":["304215"]}],"id":[{"id":"10.13039\/501100003151","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":[[2022,1,16]]},"abstract":"<jats:p>We describe the foundation of the metaprogramming language, M\u0153bius, which supports the generation of polymorphic code and, more importantly, the analysis of polymorphic code via pattern matching.<\/jats:p>\n          <jats:p>M\u0153bius has two main ingredients: 1) we exploit contextual modal types to describe open code together with the context in which it is meaningful. In M\u0153bius, open code can depend on type and term variables (level 0) whose values are supplied at a later stage, as well as code variables (level 1) that stand for code templates supplied at a later stage. This leads to a multi-level modal lambda-calculus that supports System-F style polymorphism and forms the basis for polymorphic code generation. 2) we extend the multi-level modal lambda-calculus to support pattern matching on code. As pattern matching on polymorphic code may refine polymorphic type variables, we extend our type-theoretic foundation to generate and track typing constraints that arise. We also give an operational semantics and prove type preservation.<\/jats:p>\n          <jats:p>Our multi-level modal foundation for M\u0153bius provides the appropriate abstractions for both generating and pattern matching on open code without committing to a concrete representation of variable binding and contexts. Hence, our work is a step towards building a general type-theoretic foundation for multi-staged metaprogramming that, on the one hand, enforces strong type guarantees and, on the other hand, makes it easy to generate and manipulate code. This will allow us to exploit the full potential of metaprogramming without sacrificing the reliability of and trust in the code we are producing and running.<\/jats:p>","DOI":"10.1145\/3498700","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["M\u0153bius: metaprogramming using contextual types: the stage where system f can pattern match on itself"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6338-2155","authenticated-orcid":false,"given":"Junyoung","family":"Jang","sequence":"first","affiliation":[{"name":"McGill University, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6070-485X","authenticated-orcid":false,"given":"Samuel","family":"G\u00e9lineau","sequence":"additional","affiliation":[{"name":"SimSpace, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7597-5273","authenticated-orcid":false,"given":"Stefan","family":"Monnier","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Montr\u00e9al, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2549-4276","authenticated-orcid":false,"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University, Canada"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.71.3"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837623"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944730"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005617"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561317"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"e_1_2_2_10_1","volume-title":"Moebius: Metaprogramming using Contextual Types \u2013 The stage where System F can pattern match on itself (Long Version). arxiv:2111.08099.","author":"Jang Junyoung","year":"2021","unstructured":"Junyoung Jang , Samuel G\u00e9lineau , Stefan Monnier , and Brigitte Pientka . 2021 . Moebius: Metaprogramming using Contextual Types \u2013 The stage where System F can pattern match on itself (Long Version). arxiv:2111.08099. Junyoung Jang, Samuel G\u00e9lineau, Stefan Monnier, and Brigitte Pientka. 2021. Moebius: Metaprogramming using Contextual Types \u2013 The stage where System F can pattern match on itself (Long Version). arxiv:2111.08099."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_4"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111060"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_15"},{"key":"e_1_2_2_14_1","volume-title":"8th International Logic Programming Conference. MIT Press, 255\u2013269","author":"Miller Dale","year":"1991","unstructured":"Dale Miller . 1991 . Unification of Simply Typed Lambda-Terms as Logic Programming . In 8th International Logic Programming Conference. MIT Press, 255\u2013269 . Dale Miller. 1991. Unification of Simply Typed Lambda-Terms as Logic Programming. In 8th International Logic Programming Conference. MIT Press, 255\u2013269."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158101"},{"key":"e_1_2_2_17_1","volume-title":"Tabled higher-order logic programming. Ph. D. Dissertation. Department of Computer Science","author":"Pientka Brigitte","unstructured":"Brigitte Pientka . 2003. Tabled higher-order logic programming. Ph. D. Dissertation. Department of Computer Science , Carnegie Mellon University . CMU-CS-03-185 Brigitte Pientka. 2003. Tabled higher-order logic programming. Ph. D. Dissertation. Department of Computer Science, Carnegie Mellon University. CMU-CS-03-185"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328483"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785683"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_18"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_28"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/328690.328697"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604134"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41582-1_10"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173709"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498700","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498700","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498700"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":29,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498700"],"URL":"https:\/\/doi.org\/10.1145\/3498700","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}