{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T16:59:44Z","timestamp":1776445184388,"version":"3.51.2"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,2,28]],"date-time":"2017-02-28T00:00:00Z","timestamp":1488240000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Hackett Studentship from the University of Western Australia"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2017,2,28]]},"abstract":"<jats:p>\n            This article demonstrates that there is a fundamental relationship between temporal logic and languages that involve multiple stages, such as those used to analyze binding times in the context of partial evaluation. This relationship is based on an extension of the Curry-Howard isomorphism, which identifies proofs with programs, and propositions with types. Our extension involves the \u201cnext time\u201d (\u25cb) operator from linear-time temporal logic and yields a \u03bb-calculus \u03bb\u00b0 with types of the form \u25cb\n            <jats:italic>A<\/jats:italic>\n            for expressions in the subsequent stage, with appropriate introduction and elimination forms. We demonstrate that \u03bb\u00b0 is equivalent to the core of a previously studied multilevel binding-time analysis. This is similar to work by Davies and Pfenning on staged computation based on the necessity (\u25a1) operator of modal logic, but \u25a1 only allows closed code, and naturally supports a code evaluation construct, whereas \u25cb captures open code, thus is more flexible, but is incompatible with such a construct. Instead, code evaluation is an external global operation that is validated by the proof theory regarding closed proofs of \u25cb formulas. We demonstrate the relevance of \u03bb\u00b0 to staged computation directly by showing that that normalization can be done in an order strictly following the times of the logic. We also extend \u03bb\u00b0 to small functional language and show that it would serve as a suitable basis for directly programming with multiple stages by presenting some example programs.\n          <\/jats:p>","DOI":"10.1145\/3011069","type":"journal-article","created":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T14:54:11Z","timestamp":1490367251000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["A Temporal Logic Approach to Binding-Time Analysis"],"prefix":"10.1145","volume":"64","author":[{"given":"Rowan","family":"Davies","sequence":"first","affiliation":[{"name":"University of Western Australia, Sydney NSW, Australia"}]}],"member":"320","published-online":{"date-parts":[[2017,3,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.6.685"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201999)","author":"Bawden Alan","year":"1999","unstructured":"Alan Bawden . 1999 . Quasiquotation in Lisp . In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201999) . ACM, New York, NY, 4--12. Alan Bawden. 1999. Quasiquotation in Lisp. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM\u201999). ACM, New York, NY, 4--12."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Workshop on Intuitionistic Modal Logics and Applications (IMLA\u201999)","author":"El-Abidine Benaissa Zine","year":"1999","unstructured":"Zine El-Abidine Benaissa , Eugenio Moggi , Walid Taha , and Tim Sheard . 1999 . Logical modalities and multi-stage programming . In Proceedings of the Workshop on Intuitionistic Modal Logics and Applications (IMLA\u201999) . Zine El-Abidine Benaissa, Eugenio Moggi, Walid Taha, and Tim Sheard. 1999. Logical modalities and multi-stage programming. In Proceedings of the Workshop on Intuitionistic Modal Logics and Applications (IMLA\u201999)."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898002998"},{"key":"e_1_2_1_5_1","volume-title":"Programming Language Implementation and Logic Programming","author":"Birkedal Lars","unstructured":"Lars Birkedal and Morten Welinder . 1994. Hand-writing program generator generators . In Programming Language Implementation and Logic Programming . Springer , 198--214. Lars Birkedal and Morten Welinder. 1994. Hand-writing program generator generators. In Programming Language Implementation and Logic Programming. Springer, 198--214."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.3.339"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90002-F"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004598"},{"key":"e_1_2_1_10_1","volume-title":"Generative Programming and Component Engineering","author":"Calcagno Cristiano","unstructured":"Cristiano Calcagno , Walid Taha , Liwen Huang , and Xavier Leroy . 2003b. Implementing multi-stage languages using ASTs, Gensym, and reflection . In Generative Programming and Component Engineering . Springer , 57--76. Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. 2003b. Implementing multi-stage languages using ASTs, Gensym, and reflection. In Generative Programming and Component Engineering. Springer, 57--76."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319847"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237784"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/788018.788825"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237788"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/645815.668894"},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Typed Lambda Calculi and Applications","author":"Filinski Andrzej","unstructured":"Andrzej Filinski . 2001. Normalization by evaluation for the computational lambda-calculus . In Typed Lambda Calculi and Applications . Lecture Notes in Computer Science , Vol. 2044 . Springer , 151--165. Andrzej Filinski. 2001. Normalization by evaluation for the computational lambda-calculus. In Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, Vol. 2044. Springer, 151--165."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275370"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science","volume-title":"Programming Languages: Implementations, Logics and Programs","author":"Gl\u00fcck Robert","unstructured":"Robert Gl\u00fcck and Jesper J\u00f8rgensen . 1995. Efficient multi-level generating extensions for program specialization . In Programming Languages: Implementations, Logics and Programs . Lecture Notes in Computer Science , Vol. 982 . Springer , 259--278. Robert Gl\u00fcck and Jesper J\u00f8rgensen. 1995. Efficient multi-level generating extensions for program specialization. In Programming Languages: Implementations, Logics and Programs. Lecture Notes in Computer Science, Vol. 982. Springer, 259--278."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000058"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003378"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/646445.692173"},{"key":"e_1_2_1_27_1","volume-title":"To H. B. Curry: Essays on Combinatory Logic","author":"Howard William A.","year":"1980","unstructured":"William A. Howard . 1980. The formulae-as-types notion of construction . In To H. B. Curry: Essays on Combinatory Logic , Lambda Calculus and Formalism, 1980 , J. P. Seldin and J. R. Hindley (Eds.). Academic Press , 479--490. Hitherto unpublished note of 1969, rearranged, corrected, and annotated by Howard, 1979. William A. Howard. 1980. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980, J. P. Seldin and J. R. Hindley (Eds.). Academic Press, 479--490. Hitherto unpublished note of 1969, rearranged, corrected, and annotated by Howard, 1979."},{"key":"e_1_2_1_28_1","first-page":"135","article-title":"The virtues of eta-expansion","volume":"5","author":"Barry Jay C.","year":"1996","unstructured":"C. Barry Jay and Neil Ghani . 1996 . The virtues of eta-expansion . Journal of Functional Programming 5 , 2, 135 -- 154 . C. Barry Jay and Neil Ghani. 1996. The virtues of eta-expansion. Journal of Functional Programming 5, 2, 135--154.","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_1_29_1","series-title":"Lecture Notes in Computer Science","volume-title":"ESOP 2004: Programming Languages and Systems","author":"Jia Limin","unstructured":"Limin Jia and David Walker . 2004. Modal proofs as distributed programs . In ESOP 2004: Programming Languages and Systems . Lecture Notes in Computer Science , Vol. 4514 . Springer , 219--233. Limin Jia and David Walker. 2004. Modal proofs as distributed programs. In ESOP 2004: Programming Languages and Systems. Lecture Notes in Computer Science, Vol. 4514. Springer, 219--233."},{"key":"e_1_2_1_30_1","volume-title":"Partial Evaluation and Automatic Program Generation","author":"Jones Neil D.","unstructured":"Neil D. Jones , Carsten K. Gomard , and Peter Sestoft . 1993. Partial Evaluation and Automatic Program Generation . Prentice Hall . Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice Hall."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111060"},{"key":"e_1_2_1_32_1","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Science Logic","author":"Maier Patrick","unstructured":"Patrick Maier . 2004. Intuitionistic LTL and a new characterization of safety and liveness . In Computer Science Logic . Lecture Notes in Computer Science , Vol. 3210 . Springer , 295--309. Patrick Maier. 2004. Intuitionistic LTL and a new characterization of safety and liveness. In Computer Science Logic. Lecture Notes in Computer Science, Vol. 3210. Springer, 295--309."},{"key":"e_1_2_1_34_1","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f Per","year":"1996","unstructured":"Per Martin-L\u00f6f . 1996 . On the meanings of the logical constants and the justifications of the logical laws . Nordic Journal of Philosophical Logic 1 , 1, 11 -- 60 . Per Martin-L\u00f6f. 1996. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic 1, 1, 11--60.","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"e_1_2_1_35_1","volume-title":"Proof Theory of Modal Logics","author":"Martini Simone","unstructured":"Simone Martini and Andrea Masini . 1996. A computational interpretation of modal proofs . In Proof Theory of Modal Logics , H. Wansing (Ed.). Applied Logic Series, Vol . 2. Kluwer , 213--241. Simone Martini and Andrea Masini. 1996. A computational interpretation of modal proofs. In Proof Theory of Modal Logics, H. Wansing (Ed.). Applied Logic Series, Vol. 2. Kluwer, 213--241."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90029-Y"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77353"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80155-0"},{"key":"e_1_2_1_40_1","volume-title":"Zine El-Abidine Benaissa, and Tim Sheard","author":"Moggi Eugenio","year":"1999","unstructured":"Eugenio Moggi , Walid Taha , Zine El-Abidine Benaissa, and Tim Sheard . 1999 . An idealized MetaML: Simpler, and more expressive. In Programming Languages and Systems. Springer , 193--207. Eugenio Moggi, Walid Taha, Zine El-Abidine Benaissa, and Tim Sheard. 1999. An idealized MetaML: Simpler, and more expressive. In Programming Languages and Systems. Springer, 193--207."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581498"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680500568X"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_44_1","volume-title":"Two-Level Functional Languages","author":"Nielson Flemming","unstructured":"Flemming Nielson and Hanne Riis Nielson . 1992. Two-Level Functional Languages . Cambridge University Press . Flemming Nielson and Hanne Riis Nielson. 1992. Two-Level Functional Languages. Cambridge University Press."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000770"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/788017.788741"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 11th Conference on Mathematical Foundations of Programming Semantics.","author":"Pfenning Frank","year":"1995","unstructured":"Frank Pfenning and Hao-Chi Wong . 1995 . On a modal \u03bb-calculus for S4 . In Proceedings of the 11th Conference on Mathematical Foundations of Programming Semantics. Frank Pfenning and Hao-Chi Wong. 1995. On a modal \u03bb-calculus for S4. In Proceedings of the 11th Conference on Mathematical Foundations of Programming Semantics."},{"key":"e_1_2_1_49_1","volume-title":"Natural Deduction. Almquist 8 Wiksell","author":"Prawitz Dag","unstructured":"Dag Prawitz . 1965. Natural Deduction. Almquist 8 Wiksell , Stockholm, Sweden . Dag Prawitz. 1965. Natural Deduction. Almquist 8 Wiksell, Stockholm, Sweden."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 4th International Workshop on Logic and Engineering of Natural Language Semantics. 167--178","author":"Shan Chung-Chieh","year":"2007","unstructured":"Chung-Chieh Shan . 2007 . Inverse scope as metalinguistic quotation in operational semantics . In Proceedings of the 4th International Workshop on Logic and Engineering of Natural Language Semantics. 167--178 . Chung-Chieh Shan. 2007. Inverse scope as metalinguistic quotation in operational semantics. In Proceedings of the 4th International Workshop on Logic and Engineering of Natural Language Semantics. 167--178."},{"key":"e_1_2_1_52_1","volume-title":"Handbook of Logic in Computer Science","author":"Stirling Colin","unstructured":"Colin Stirling . 1992. Modal and temporal logics . In Handbook of Logic in Computer Science , Vol. 2 . Oxford University Press , Oxford, UK , 477--563. Colin Stirling. 1992. Modal and temporal logics. In Handbook of Logic in Computer Science, Vol. 2. Oxford University Press, Oxford, UK, 477--563."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604134"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259019"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_25"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1140335.1140360"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011069","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3011069","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:35Z","timestamp":1750220615000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011069"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,28]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,2,28]]}},"alternative-id":["10.1145\/3011069"],"URL":"https:\/\/doi.org\/10.1145\/3011069","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,28]]},"assertion":[{"value":"2007-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-03-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}