{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T16:59:42Z","timestamp":1776445182113,"version":"3.51.2"},"reference-count":31,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2010,12,18]],"date-time":"2010-12-18T00:00:00Z","timestamp":1292630400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Taha and Nielsen have developed a multi-stage calculus {\\lambda}{\\alpha} with\na sound type system using the notion of environment classifiers. They are\nspecial identifiers, with which code fragments and variable declarations are\nannotated, and their scoping mechanism is used to ensure statically that\ncertain code fragments are closed and safely runnable. In this paper, we\ninvestigate the Curry-Howard isomorphism for environment classifiers by\ndeveloping a typed {\\lambda}-calculus {\\lambda}|&gt;. It corresponds to\nmulti-modal logic that allows quantification by transition variables---a\ncounterpart of classifiers---which range over (possibly empty) sequences of\nlabeled transitions between possible worlds. This interpretation will reduce\nthe \"run\" construct---which has a special typing rule in\n{\\lambda}{\\alpha}---and embedding of closed code into other code fragments of\ndifferent stages---which would be only realized by the cross-stage persistence\noperator in {\\lambda}{\\alpha}---to merely a special case of classifier\napplication. {\\lambda}|&gt; enjoys not only basic properties including subject\nreduction, confluence, and strong normalization but also an important property\nas a multi-stage calculus: time-ordered normalization of full reduction. Then,\nwe develop a big-step evaluation semantics for an ML-like language based on\n{\\lambda}|&gt; with its type system and prove that the evaluation of a well-typed\n{\\lambda}|&gt; program is properly staged. We also identify a fragment of the\nlanguage, where erasure evaluation is possible. Finally, we show that the proof\nsystem augmented with a classical axiom is sound and complete with respect to a\nKripke semantics of the logic.<\/jats:p>","DOI":"10.2168\/lmcs-6(4:8)2010","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T13:29:57Z","timestamp":1316784597000},"source":"Crossref","is-referenced-by-count":6,"title":["A Logical Foundation for Environment Classifiers"],"prefix":"10.46298","volume":"Volume 6, Issue 4","author":[{"given":"Takeshi","family":"Tsukada","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"}]}],"member":"25203","published-online":{"date-parts":[[2010,12,18]]},"reference":[{"key":"10.2168\/LMCS-6(4:8)2010_JonesGomardSestoft93PEbook","unstructured":"Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall (1993)"},{"key":"10.2168\/LMCS-6(4:8)2010_ConselLawallLeMeur04SCP","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.03.011"},{"key":"10.2168\/LMCS-6(4:8)2010_WicklineLeePfenning98PLDI","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277727"},{"key":"10.2168\/LMCS-6(4:8)2010_PolettoHsiehEnglerKaashoek99TOPLAS","doi-asserted-by":"publisher","DOI":"10.1145\/316686.316697"},{"key":"10.2168\/LMCS-6(4:8)2010_TahaSheard00TCS","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"10.2168\/LMCS-6(4:8)2010_GlueckJorgensen95PLILP","unstructured":"Gl\u00fcck, R., J\u00f8rgensen, J.: Efficient multi-level generating extensions for program specialization. In: Proceedings of Programming Languages, Implementations, Logics and Programs (PLILP'95). Volume 982 of LNCS. (1995) 259-278"},{"key":"10.2168\/LMCS-6(4:8)2010_Davies-Atemporallogicappro","unstructured":"Davies, R.: A temporal-logic approach to binding-time analysis. In: Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS 1996), IEEE Computer Society Press (1996) 184-195"},{"key":"10.2168\/LMCS-6(4:8)2010_Davies2001","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"10.2168\/LMCS-6(4:8)2010_604134","unstructured":"Taha, W., Nielsen, M.F.: Environment classifiers. In: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '03), New York, NY, USA, ACM (2003) 26-37"},{"key":"10.2168\/LMCS-6(4:8)2010_Yuse2006","doi-asserted-by":"publisher","DOI":"10.1145\/1140335.1140360"},{"key":"10.2168\/LMCS-6(4:8)2010_1111060","unstructured":"Kim, I.S., Yi, K., Calcagno, C.: A polymorphic modal type system for lisp-like multi-staged languages. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '06), New York, NY, USA, ACM (2006) 257-268"},{"key":"10.2168\/LMCS-6(4:8)2010_DBLP:conf\/popl\/DaviesP96","unstructured":"Davies, R., Pfenning, F.: A modal analysis of staged computation. In: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '96). (1996) 258-270"},{"key":"10.2168\/LMCS-6(4:8)2010_StirlingHandbook","unstructured":"Stirling, C.: Modal and temporal logics. In: Handbook of Logic in Computer Science. Volume 2. Oxford University Press (1992) 477-563"},{"key":"10.2168\/LMCS-6(4:8)2010_MoggiTahaBenaissaSheard99ESOP","unstructured":"Moggi, E., Taha, W., Benaissa, Z.E.A., Sheard, T.: An idealized MetaML: Simpler, and more expressive. In: Proceedings of European Symposium on Programming (ESOP'99). Volume 1576 of LNCS. (1999) 193-207"},{"key":"10.2168\/LMCS-6(4:8)2010_BenaissaMoggiTahaSheard99IMLA","unstructured":"Benaissa, Z.E.A., Moggi, E., Taha, W., Sheard, T.: Logical modalities and multi-stage programming. In: Proceedings of Workshop on Intuitionistic Modal Logics and Applications (IMLA'99). (1999)"},{"key":"10.2168\/LMCS-6(4:8)2010_Calcagno2004","unstructured":"Calcagno, C., Moggi, E., Taha, W.: ML-like inference for classifiers. In: Proceedings of European Symposium on Programming (ESOP '04), Springer-Verlag (2004) 79-93"},{"key":"10.2168\/LMCS-6(4:8)2010_PlotkinStirling86TARK","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Stirling, C.: A framework for intuitionistic modal logics. In: Proceedings of Theoretical Aspects of Reasoning about Knowledge, Monterey, CA, Morgan Kaufmann (1986)","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"10.2168\/LMCS-6(4:8)2010_KojimaIgarashi08IMLA","unstructured":"Kojima, K., Igarashi, A.: On constructive linear-time temporal logic. In: Proceedings of Intuitionistic Modal Logics and Applications Workshop (IMLA '08), Pittsburgh, PA (2008)"},{"key":"10.2168\/LMCS-6(4:8)2010_KojimaIgarashi10IC","doi-asserted-by":"crossref","unstructured":"Kojima, K., Igarashi, A.: Constructive linear-time temporal logic: Proof systems and Kripke semantics. Information and Computation (2010) Accepted for publication.","DOI":"10.1016\/j.ic.2010.09.008"},{"key":"10.2168\/LMCS-6(4:8)2010_DBLP:journals\/iandc\/Takahashi95","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"10.2168\/LMCS-6(4:8)2010_NanevskiPfenning05JFP","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680500568X"},{"key":"10.2168\/LMCS-6(4:8)2010_CalcagnoMoggiSheard03JFP","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004598"},{"key":"10.2168\/LMCS-6(4:8)2010_SatoSakuraiKameyama01JFLP","unstructured":"Sato, M., Sakurai, T., Kameyama, Y.: A simply typed context calculus with first-class environments. Journal of Functional and Logic Programming 2002(4) (2002) 1-41"},{"key":"10.2168\/LMCS-6(4:8)2010_NanevskiPfenningPientka08TOCL","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"10.2168\/LMCS-6(4:8)2010_VieraPardo06GPCE","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173709"},{"key":"10.2168\/LMCS-6(4:8)2010_KameyamaKiselyovShan09PEPM","doi-asserted-by":"crossref","unstructured":"Kameyama, Y., Kiselyov, O., chieh Shan, C.: Shifting the stage: Staging with delimited control. In: Proceedings of ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'09), Savannah, GA (2009)","DOI":"10.1145\/1328408.1328430"},{"key":"10.2168\/LMCS-6(4:8)2010_DanvyFilinski90LFP","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"10.2168\/LMCS-6(4:8)2010_LawallDanvy94LFP","doi-asserted-by":"publisher","DOI":"10.1145\/182409.182483"},{"key":"10.2168\/LMCS-6(4:8)2010_dynamiclogic","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In Gabbay, D., Guenther, F., eds.: Handbook of Philosophical Logic. Volume 4. 2nd edn. Springer-Verlag (2002) 99-218"},{"key":"10.2168\/LMCS-6(4:8)2010_hybridlogic","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In Blackburn, P., Wolter, F., van Benthem, J., eds.: Handbook of Modal Logics. Elsevier (2006) 821-868"},{"key":"10.2168\/LMCS-6(4:8)2010_ReedPfenning07M4M","unstructured":"Reed, J., Pfenning, F.: Intuitionistic letcc via labelled deduction. In: Proceedings of Workshop on Methods for Modalities (M4M). (2007)"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1065\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1065\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:27Z","timestamp":1681243347000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1065"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,12,18]]},"references-count":31,"URL":"https:\/\/doi.org\/10.2168\/lmcs-6(4:8)2010","relation":{"is-same-as":[{"id-type":"arxiv","id":"1010.3806","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1010.3806","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,12,18]]},"article-number":"1065"}}