{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:14:01Z","timestamp":1775790841220,"version":"3.50.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031300431","type":"print"},{"value":"9783031300448","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T00:00:00Z","timestamp":1681689600000},"content-version":"vor","delay-in-days":106,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"Abstract<\/jats:title>Modal types\u2014types that are derived from proof systems of modal logic\u2014have been studied as theoretical foundations of metaprogramming, where program code is manipulated as first-class values. In modal type systems, modality corresponds to a type constructor for code types and controls free variables and their types in code values. Nanevski et al. have proposed contextual modal type theory<\/jats:italic>, which has modal types with fine-grained information on free variables: modal types are explicitly indexed by contexts<\/jats:italic>\u2014the types of all free variables in code values.<\/jats:p>This paper presents $$\\lambda _{\\forall []}$$<\/jats:tex-math>\n \n \u03bb<\/mml:mi>\n \n \u2200<\/mml:mo>\n [<\/mml:mo>\n ]<\/mml:mo>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, a novel extension of contextual modal type theory with parametric polymorphism over contexts<\/jats:italic>. Such an extension has been studied in the literature but, unlike earlier proposals, $$\\lambda _{\\forall []}$$<\/jats:tex-math>\n \n \u03bb<\/mml:mi>\n \n \u2200<\/mml:mo>\n [<\/mml:mo>\n ]<\/mml:mo>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is more general in that it allows multiple occurrence of context variables in a single context. We formalize $$\\lambda _{\\forall []}$$<\/jats:tex-math>\n \n \u03bb<\/mml:mi>\n \n \u2200<\/mml:mo>\n [<\/mml:mo>\n ]<\/mml:mo>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> with its type system and operational semantics given by $$\\beta $$<\/jats:tex-math>\n \u03b2<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-reduction and prove its basic properties including subject reduction, strong normalization, and confluence. Moreover, to demonstrate the expressive power of polymorphic contexts, we show a type-preserving embedding from a two-level fragment of Davies\u2019 $$\\lambda _{\\bigcirc }$$<\/jats:tex-math>\n \n \u03bb<\/mml:mi>\n \u25ef<\/mml:mo>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, which is based on linear-time temporal logic, to $$\\lambda _{\\forall []}$$<\/jats:tex-math>\n \n \u03bb<\/mml:mi>\n \n \u2200<\/mml:mo>\n [<\/mml:mo>\n ]<\/mml:mo>\n <\/mml:mrow>\n <\/mml:msub>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> .<\/jats:p>","DOI":"10.1007\/978-3-031-30044-8_11","type":"book-chapter","created":{"date-parts":[[2023,4,16]],"date-time":"2023-04-16T20:28:25Z","timestamp":1681676905000},"page":"281-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Contextual Modal Type Theory with Polymorphic Contexts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6038-6249","authenticated-orcid":false,"given":"Yuito","family":"Murase","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8944-5924","authenticated-orcid":false,"given":"Yuichi","family":"Nishiwaki","sequence":"additional","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"}]}],"member":"297","published-online":{"date-parts":[[2023,4,17]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Borghuis, V.A.J.: Coming to terms with modal logic: on the interpretation of modalities in typed lambda-calculus. Ph.D. thesis, Technische Universiteit Eindhoven (1994). https:\/\/doi.org\/10.6100\/IR427575","DOI":"10.6100\/IR427575"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Taha, W., Huang, L., Leroy, X.: Implementing multi-stage languages using ASTs, gensym, and reflection. In: Pfenning, F., Smaragdakis, Y. (eds.) Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02830, pp. 57\u201376. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-39815-8_4","DOI":"10.1007\/978-3-540-39815-8_4"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Cave, A., Pientka, B.: First-class substitutions in contextual type theory. In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-Languages: Theory & Practice. pp. 15\u201324. LFMTP \u201913, Association for Computing Machinery, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2503887.2503889","DOI":"10.1145\/2503887.2503889"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Clouston, R.: Fitch-style modal lambda calculi. In: Baier, C., Dal\u00a0Lago, U. (eds.) Proc. of Foundations of Software Science and Computation Structures. pp. 258\u2013275. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89366-2_14","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Davies, R.: A temporal logic approach to binding-time analysis. J. ACM 64(1) (Mar 2017). https:\/\/doi.org\/10.1145\/3011069","DOI":"10.1145\/3011069"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. J. ACM 48(3), 555\u2013604 (May 2001). https:\/\/doi.org\/10.1145\/382780.382785","DOI":"10.1145\/382780.382785"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Ganz, S.E., Sabry, A., Taha, W.: Macros as multi-stage computations: Type-safe, generative, binding macros in macroml. In: Pierce, B.C. (ed.) Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming (ICFP \u201901), Firenze (Florence), Italy, September 3-5, 2001. pp. 74\u201385. ACM (2001). https:\/\/doi.org\/10.1145\/507635.507646","DOI":"10.1145\/507635.507646"},{"key":"11_CR8","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (1989)"},{"key":"11_CR9","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) (Jan 2022). https:\/\/doi.org\/10.1145\/3498700","DOI":"10.1145\/3498700"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Kameyama, Y., Kiselyov, O., Shan, C.: Closing the stage: From staged code to typed closures. In: PEPM\u201908 \u2013 Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. pp. 147\u2013157 (Dec 2008). https:\/\/doi.org\/10.1145\/1328408.1328430","DOI":"10.1145\/1328408.1328430"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Kavvos, G.A.: Dual-context calculi for modal logic. In: Proc. of the 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201312 (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005089","DOI":"10.1109\/LICS.2017.8005089"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Kim, I., Yi, K., Calcagno, C.: A polymorphic modal type system for lisp-like multi-staged languages. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006. pp. 257\u2013268. ACM (2006). https:\/\/doi.org\/10.1145\/1111037.1111060","DOI":"10.1145\/1111037.1111060"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Kiselyov, O.: The design and implementation of BER MetaOCaml: System description. In: Codish, M., Sumii, E. (eds.) Functional and Logic Programming \u2013 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08475, pp. 86\u2013102. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-07151-0_6","DOI":"10.1007\/978-3-319-07151-0_6"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Kiselyov, O., Kameyama, Y., Sudo, Y.: Refined environment classifiers. In: Igarashi, A. (ed.) Proc. of Asian Symposium on Programming Languages and Systems. pp. 271\u2013291. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_15","DOI":"10.1007\/978-3-319-47958-3_15"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Martini, S., Masini, A.: A computational interpretation of modal proofs. In: Proof Theory of Modal Logic, pp. 213\u2013241. Springer Netherlands, Dordrecht (1996). https:\/\/doi.org\/10.1007\/978-94-017-2798-3_12","DOI":"10.1007\/978-94-017-2798-3_12"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Pfenning, F.: Staged computation with names and necessity. J. Funct. Program. 15(6), 893\u2013939 (Nov 2005). https:\/\/doi.org\/10.1017\/S095679680500568X","DOI":"10.1017\/S095679680500568X"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Trans. Comput. Logic 9(3) (Jun 2008). https:\/\/doi.org\/10.1145\/1352582.1352591","DOI":"10.1145\/1352582.1352591"},{"key":"11_CR18","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) (Dec 2017). https:\/\/doi.org\/10.1145\/3158101","DOI":"10.1145\/3158101"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical. Structures in Comp. Sci. 11(4), 511\u2013540 (Aug 2001). https:\/\/doi.org\/10.1017\/S0960129501003322","DOI":"10.1017\/S0960129501003322"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Giesl, J., H\u00e4hnle, R. (eds.) Automated Reasoning. pp. 15\u201321. Springer Berlin Heidelberg, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_2","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Pientka, B., Thibodeau, D., Abel, A., Ferreira, F., Zucchini, R.: A type theory for defining logics and proofs. In: Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science. LICS \u201919, IEEE Press (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785683","DOI":"10.1109\/LICS.2019.8785683"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Pretnar, M.: Handlers of algebraic effects. In: Castagna, G. (ed.) Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05502, pp. 80\u201394. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-00590-9_7","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"11_CR23","unstructured":"Puech, M.: A contextual account of staged computations (2016), preprint on webpage at http:\/\/cedric.cnam.fr\/~puechm\/draft_contextual.pdf"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Rhiger, M.: Staged computation with staged lexical scope. In: Seidl, H. (ed.) Programming Languages and Systems - 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. Lecture Notes in Computer Science, 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":"11_CR25","doi-asserted-by":"publisher","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: The Curry\u2013Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, vol.\u00a0149, chap.\u00a04, pp. 77\u2013101. Elsevier (2006). https:\/\/doi.org\/10.1016\/S0049-237X(06)80005-4, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0049237X06800054","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Stampoulis, A., Shao, Z.: VeriML: Typed computation of logical terms inside a language with effects. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming. pp. 333\u2013344. ICFP \u201910, Association for Computing Machinery, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1863543.1863591","DOI":"10.1145\/1863543.1863591"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Stucki, N., Biboudis, A., Odersky, M.: A practical unification of multi-stage programming and macros pp. 14\u201327 (2018). https:\/\/doi.org\/10.1145\/3278122.3278139","DOI":"10.1145\/3278122.3278139"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Stucki, N., Brachth\u00e4user, J.I., Odersky, M.: Multi-stage programming with generative and analytical macros. In: Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences. p. 110\u2013122. GPCE 2021, Association for Computing Machinery, New York, NY, USA (2021). https:\/\/doi.org\/10.1145\/3486609.3487203, https:\/\/doi.org\/10.1145\/3486609.3487203","DOI":"10.1145\/3486609.3487203"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Taha, W., Nielsen, M.F.: Environment classifiers. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 26\u201337. POPL \u201903, Association for Computing Machinery, New York, NY, USA (2003). https:\/\/doi.org\/10.1145\/604131.604134","DOI":"10.1145\/604131.604134"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Tsukada, T., Igarashi, A.: A logical foundation for environment classifiers. Log. Methods Comput. Sci. 6(4) (2010). https:\/\/doi.org\/10.2168\/LMCS-6(4:8)2010","DOI":"10.2168\/LMCS-6(4:8)2010"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Valliappan, N., Ruch, F., Tom\u00e9 Corti\u00f1as, C.: Normalization for fitch-style modal calculi. Proc. ACM Program. Lang. 6(ICFP) (Aug 2022). https:\/\/doi.org\/10.1145\/3547649","DOI":"10.1145\/3547649"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Zyuzin, N., Nanevski, A.: Contextual modal types for algebraic effects and handlers. Proc. ACM Program. Lang. 5(ICFP) (Aug 2021). https:\/\/doi.org\/10.1145\/3473580","DOI":"10.1145\/3473580"}],"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-031-30044-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T09:04:05Z","timestamp":1686128645000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30044-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031300431","9783031300448"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30044-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"55","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}