{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T05:57:14Z","timestamp":1777874234718,"version":"3.51.4"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227195","type":"print"},{"value":"9783032227201","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":99,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22720-1_2","type":"book-chapter","created":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T15:30:33Z","timestamp":1775748633000},"page":"13-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Contextual Metaprogramming for Session Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7849-195X","authenticated-orcid":false,"given":"Pedro","family":"\u00c2ngelo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5143-9764","authenticated-orcid":false,"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6038-6249","authenticated-orcid":false,"given":"Yuito","family":"Murase","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9539-8861","authenticated-orcid":false,"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Fiore, M.P.: Syntactic considerations on recursive types. In: LICS. pp. 242\u2013252. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561324","DOI":"10.1109\/LICS.1996.561324"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Almeida, B., Mordido, A., Thiemann, P., Vasconcelos, V.T.: Polymorphic lambda calculus with context-free session types. Inf. Comput. 289(Part), 104948 (2022). https:\/\/doi.org\/10.1016\/J.IC.2022.104948","DOI":"10.1016\/J.IC.2022.104948"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"\u00c2ngelo, P., Igarashi, A., Murase, Y., Vasconcelos, V.T.: Contextual metaprogramming for session types. CoRR abs\/2601.15180 (2026). https:\/\/doi.org\/10.48550\/arXiv.2601.15180","DOI":"10.48550\/arXiv.2601.15180"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"\u00c2ngelo, P., Igarashi, A., Vasconcelos, V.T.: Linear contextual metaprogramming and session types. In: PLACES. EPTCS, vol.\u00a0401, pp. 1\u201310 (2024). https:\/\/doi.org\/10.4204\/EPTCS.401.1","DOI":"10.4204\/EPTCS.401.1"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Balat, V.: Ocsigen: typing web interaction with objective caml. In: Workshop on ML. pp. 84\u201394. ACM (2006). https:\/\/doi.org\/10.1145\/1159876.1159889","DOI":"10.1145\/1159876.1159889"},{"key":"2_CR6","unstructured":"Barendregt, H.P.: The lambda calculus - its syntax and semantics, Studies in logic and the foundations of mathematics, vol.\u00a0103. North-Holland (1985)"},{"key":"2_CR7","unstructured":"Boinc. https:\/\/boinc.berkeley.edu\/, accessed: 2025-04-09"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Proceedings of CONCUR. LNCS, vol.\u00a06269, pp. 222\u2013236. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Math. Struct. Comput. Sci. 26(3), 367\u2013423 (2016). https:\/\/doi.org\/10.1017\/S0960129514000218","DOI":"10.1017\/S0960129514000218"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Chun, B., Ihm, S., Maniatis, P., Naik, M., Patti, A.: Clonecloud: elastic execution between mobile device and cloud. In: EuroSys. pp. 301\u2013314. ACM (2011). https:\/\/doi.org\/10.1145\/1966445.1966473","DOI":"10.1145\/1966445.1966473"},{"key":"2_CR11","doi-asserted-by":"publisher","unstructured":"Clouston, R.: Fitch-style modal lambda calculi. In: FOSSACS. LNCS, vol. 10803, pp. 258\u2013275. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_14","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Davies, R.: A temporal logic approach to binding-time analysis. J. ACM 64(1), 1:1\u20131:45 (2017). https:\/\/doi.org\/10.1145\/3011069","DOI":"10.1145\/3011069"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555\u2013604 (2001). https:\/\/doi.org\/10.1145\/382780.382785","DOI":"10.1145\/382780.382785"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Dean, J., Ghemawat, S.: MapReduce: simplified data processing on large clusters. Commun. ACM 51(1), 107\u2013113 (2008). https:\/\/doi.org\/10.1145\/1327452.1327492","DOI":"10.1145\/1327452.1327492"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Thiemann, P., Vasconcelos, V.T.: Duality of session types: The final cut. In: PLACES. EPTCS, vol.\u00a0314, pp. 23\u201333 (2020). https:\/\/doi.org\/10.4204\/EPTCS.314.3","DOI":"10.4204\/EPTCS.314.3"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Vasconcelos, V.T.: Linear type theory for asynchronous session types. J. Funct. Program. 20(1), 19\u201350 (2010). https:\/\/doi.org\/10.1017\/S0956796809990268","DOI":"10.1017\/S0956796809990268"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Georges, A.L., Murawska, A., Otis, S., Pientka, B.: LINCX: A linear logical framework with first-class contexts. In: ESOP. LNCS, vol. 10201, pp. 530\u2013555. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_20","DOI":"10.1007\/978-3-662-54434-1_20"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Honda, K.: Types for dyadic interaction. In: CONCUR. LNCS, vol.\u00a0715, pp. 509\u2013523. Springer (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_35","DOI":"10.1007\/3-540-57208-2_35"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: ESOP. LNCS, vol.\u00a01381, pp. 122\u2013138. Springer (1998). https:\/\/doi.org\/10.1007\/BFb0053567","DOI":"10.1007\/BFb0053567"},{"key":"2_CR20","unstructured":"HTMX. https:\/\/htmx.org\/, accessed: 2025-02-22"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Hu, J.Z.S., Pientka, B.: Layered modal type theory - where meta-programming meets intensional analysis. In: ESOP. LNCS, vol. 14576, pp. 52\u201382. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57262-3_3","DOI":"10.1007\/978-3-031-57262-3_3"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Jang, J., G\u00e9lineau, S., Monnier, S., Pientka, B.: M\u0153bius: metaprogramming using contextual types: the stage where system F can pattern match on itself. Proc. ACM Program. Lang. 6(POPL), 1\u201327 (2022). https:\/\/doi.org\/10.1145\/3498700","DOI":"10.1145\/3498700"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Kameyama, Y., Kiselyov, O., Shan, C.: Shifting the stage - staging with delimited control. J. Funct. Program. 21(6), 617\u2013662 (2011). https:\/\/doi.org\/10.1017\/S0956796811000256","DOI":"10.1017\/S0956796811000256"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Kiselyov, O.: MetaOCaml theory and implementation. CoRR abs\/2309.08207 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2309.08207","DOI":"10.48550\/ARXIV.2309.08207"},{"key":"2_CR25","unstructured":"Meteor.js. https:\/\/www.meteor.com\/, accessed: 2025-04-09"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2(2), 119\u2013141 (1992). https:\/\/doi.org\/10.1017\/S0960129500001407","DOI":"10.1017\/S0960129500001407"},{"key":"2_CR27","unstructured":"Mitchell, J.C.: Foundations for programming languages. Foundation of computing series, MIT Press (1996)"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Murase, Y., Nishiwaki, Y., Igarashi, A.: Contextual modal type theory with polymorphic contexts. In: ESOP. LNCS, vol. 13990, pp. 281\u2013308. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_11","DOI":"10.1007\/978-3-031-30044-8_11"},{"key":"2_CR29","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Pfenning, F.: Staged computation with names and necessity. J. Funct. Program. 15(5), 893\u2013939 (2005). https:\/\/doi.org\/10.1017\/S095679680500568X","DOI":"10.1017\/S095679680500568X"},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Trans. Comput. Log. 9(3), 23:1\u201323:49 (2008). https:\/\/doi.org\/10.1145\/1352582.1352591","DOI":"10.1145\/1352582.1352591"},{"key":"2_CR31","unstructured":"Next.js. https:\/\/nextjs.org\/, accessed: 2025-04-09"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Parreaux, L., Voizard, A., Shaikhha, A., Koch, C.E.: Unifying analytic and statically-typed quasiquotes. Proc. ACM Program. Lang. 2(POPL), 13:1\u201313:33 (2018). https:\/\/doi.org\/10.1145\/3158101","DOI":"10.1145\/3158101"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11(4), 511\u2013540 (2001). https:\/\/doi.org\/10.1017\/S0960129501003322","DOI":"10.1017\/S0960129501003322"},{"key":"2_CR34","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press (2002)"},{"key":"2_CR35","doi-asserted-by":"publisher","unstructured":"Po\u00e7as, D., Costa, D., Mordido, A., Vasconcelos, V.T.: System f$$^\\mu $$$$\\phi $$mega with context-free session types. In: ESOP. LNCS, vol. 13990, pp. 392\u2013420. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_15","DOI":"10.1007\/978-3-031-30044-8_15"},{"key":"2_CR36","unstructured":"Prawitz, D.: Natural deduction. Almquist & Wiksell, Stockholm, Sweden (1965)"},{"key":"2_CR37","unstructured":"Primegrid. https:\/\/www.primegrid.com\/, accessed: 2025-04-09"},{"key":"2_CR38","unstructured":"React server components. https:\/\/react.dev\/reference\/rsc\/server-components, accessed: 2025-04-09"},{"key":"2_CR39","doi-asserted-by":"publisher","unstructured":"Rhiger, M.: Staged computation with staged lexical scope. In: ESOP. LNCS, vol.\u00a07211, pp. 559\u2013578. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_28","DOI":"10.1007\/978-3-642-28869-2_28"},{"key":"2_CR40","doi-asserted-by":"publisher","unstructured":"Sano, C., Garg, D., Kavanagh, R., Pientka, B., Toninho, B.: Fusing session-typed concurrent programming into functional programming. Proc. ACM Program. Lang. 9(ICFP) (Aug 2025). https:\/\/doi.org\/10.1145\/3747519, https:\/\/doi.org\/10.1145\/3747519","DOI":"10.1145\/3747519"},{"key":"2_CR41","unstructured":"Scala-loci. https:\/\/scala-loci.github.io\/, accessed: 2025-04-09"},{"key":"2_CR42","doi-asserted-by":"publisher","unstructured":"Serrano, M., Prunet, V.: A glimpse of hopjs. In: ICPF. pp. 180\u2013192. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951916","DOI":"10.1145\/2951913.2951916"},{"key":"2_CR43","doi-asserted-by":"publisher","unstructured":"Sheard, T., Jones, S.P.: Template meta-programming for haskell. In: Workshop on Haskell. pp. 1\u201316. ACM (2002). https:\/\/doi.org\/10.1145\/581690.581691","DOI":"10.1145\/581690.581691"},{"key":"2_CR44","doi-asserted-by":"publisher","unstructured":"Silva, G., Mordido, A., Vasconcelos, V.T.: Subtyping context-free session types. In: CONCUR. LIPIcs, vol.\u00a0279, pp. 11:1\u201311:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.11","DOI":"10.4230\/LIPICS.CONCUR.2023.11"},{"key":"2_CR45","doi-asserted-by":"publisher","unstructured":"Stucki, N., Brachth\u00e4user, J.I., Odersky, M.: Multi-stage programming with generative and analytical macros. In: GPCE. pp. 110\u2013122. ACM (2021). https:\/\/doi.org\/10.1145\/3486609.3487203","DOI":"10.1145\/3486609.3487203"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Taha, W., Nielsen, M.F.: Environment classifiers. In: POPL. pp. 26\u201337. ACM (2003). https:\/\/doi.org\/10.1145\/604131.604134","DOI":"10.1145\/604131.604134"},{"key":"2_CR47","doi-asserted-by":"publisher","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: PARLE. LNCS, vol.\u00a0817, pp. 398\u2013413. Springer (1994). https:\/\/doi.org\/10.1007\/3-540-58184-7_118","DOI":"10.1007\/3-540-58184-7_118"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: ICFP. pp. 462\u2013475. ACM (2016). https:\/\/doi.org\/10.1145\/2951913.2951926","DOI":"10.1145\/2951913.2951926"},{"key":"2_CR49","unstructured":"Unison. https:\/\/www.unison-lang.org\/, accessed: 2025-04-09"},{"key":"2_CR50","unstructured":"Ur\/Web. https:\/\/github.com\/urweb\/urweb, accessed: 2025-04-09"},{"key":"2_CR51","doi-asserted-by":"publisher","unstructured":"Valliappan, N., Ruch, F., Tom\u2019e Corti\u00a0nas, C.: Normalization for Fitch-style modal calculi. Proc. ACM Program. Lang. 6(ICFP), 772\u2013798 (2022). https:\/\/doi.org\/10.1145\/3547649","DOI":"10.1145\/3547649"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Vasconcelos, V.T.: Fundamentals of session types. Inf. Comput. 217, 52\u201370 (2012). https:\/\/doi.org\/10.1016\/J.IC.2012.05.002","DOI":"10.1016\/J.IC.2012.05.002"},{"key":"2_CR53","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Propositions as sessions. J. Funct. Program. 24(2-3), 384\u2013418 (2014)","DOI":"10.1017\/S095679681400001X"},{"key":"2_CR54","doi-asserted-by":"crossref","unstructured":"Walker, D.: Advanced Topics in Types and Programming Languages, chap. Substructural Type Systems, pp. 3\u201344. The MIT Press (2005)","DOI":"10.7551\/mitpress\/1104.003.0003"},{"key":"2_CR55","unstructured":"White, T.: Hadoop - The Definitive Guide: Storage and Analysis at Internet Scale (4. ed., revised & updated). O\u2019Reilly (2015)"},{"key":"2_CR56","doi-asserted-by":"publisher","unstructured":"Wood, J., Atkey, R.: A framework for substructural type systems. In: ESOP. LNCS, vol. 13240, pp. 376\u2013402. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_14","DOI":"10.1007\/978-3-030-99336-8_14"},{"key":"2_CR57","doi-asserted-by":"publisher","unstructured":"Xie, N., White, L., Nicole, O., Yallop, J.: Macocaml: Staging composable and compilable macros. Proc. ACM Program. Lang. 7(ICFP), 604\u2013648 (2023). https:\/\/doi.org\/10.1145\/3607851","DOI":"10.1145\/3607851"},{"key":"2_CR58","doi-asserted-by":"publisher","unstructured":"Zackon, D., Sano, C., Momigliano, A., Pientka, B.: Split decisions: Explicit contexts for substructural languages. In: CPP. pp. 257\u2013271. ACM (2025). https:\/\/doi.org\/10.1145\/3703595.3705888","DOI":"10.1145\/3703595.3705888"},{"key":"2_CR59","unstructured":"Zaharia, M., Chowdhury, M., Franklin, M.J., Shenker, S., Stoica, I.: Spark: Cluster computing with working sets. In: HotCloud\u201910. USENIX Association (2010)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22720-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:23:29Z","timestamp":1777577009000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22720-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227195","9783032227201"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22720-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}