{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:38:09Z","timestamp":1770284289246,"version":"3.49.0"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720186","type":"print"},{"value":"9783030720193","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose a logic for temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, represented via coinductive types. Specifications of programs use safety and liveness properties. Programs can then be proven to satisfy their specification in a compositional way, our logic being based on a type system.<\/jats:p><jats:p>The logic is presented as a refinement type system over the guarded<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03bb<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus, a<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03bb<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus with guarded recursive types. The refinements are formulae of a modal<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mu $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03bc<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-calculus which embeds usual temporal modal logics such as and . The semantics of our system is given within a rich structure, the topos of trees, in which we build a realizability model of the temporal refinement type system.<\/jats:p>","DOI":"10.1007\/978-3-030-72019-3_20","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"548-578","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Temporal Refinements for Guarded Recursive Types"],"prefix":"10.1007","author":[{"given":"Guilhem","family":"Jaber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"Riba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"20_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Pientka, B.: Well-founded recursion with copatterns and sized types. J. Funct. Program. 26, e2 (2016). https:\/\/doi.org\/10.1017\/S0956796816000022, https:\/\/doi.org\/10.1017\/S0956796816000022","DOI":"10.1017\/S0956796816000022"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Ahmed, A.: Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types. In: Proceedings of the 15th European Conference on Programming Languages and Systems. pp. 69\u201383. ESOP\u201906, Springer-Verlag, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11693024_6, https:\/\/doi.org\/10.1007\/11693024_6","DOI":"10.1007\/11693024_6"},{"key":"20_CR3","doi-asserted-by":"publisher","unstructured":"Appel, A., Melli\u00e8s, P.A., Richards, C., Vouillon, J.: A Very Modal Model of a Modern, Major, General Type System. SIGPLAN Not. 42(1), 109\u2013122 (2007). https:\/\/doi.org\/10.1145\/1190215.1190235, https:\/\/doi.org\/10.1145\/1190215.1190235","DOI":"10.1145\/1190215.1190235"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Appel, A.W., McAllester, D.: An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001). https:\/\/doi.org\/10.1145\/504709.504712, https:\/\/doi.org\/10.1145\/504709.504712","DOI":"10.1145\/504709.504712"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. pp. 197\u2013208. ICFP \u201913, ACM, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2500365.2500597","DOI":"10.1145\/2500365.2500597"},{"key":"20_CR6","doi-asserted-by":"publisher","unstructured":"Bahr, P., Grathwohl, H.B., M\u00f8gelberg, R.E.: The Clocks Are Ticking: No More Delays! In: 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201312 (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005097","DOI":"10.1109\/LICS.2017.8005097"},{"key":"20_CR7","doi-asserted-by":"publisher","unstructured":"Bahr, P., Graulund, C., M\u00f8gelberg, R.: Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks. Proc. ACM Program. Lang. 3(ICFP), 109:1\u2013109:27 (2019). https:\/\/doi.org\/10.1145\/3341713","DOI":"10.1145\/3341713"},{"key":"20_CR8","unstructured":"Bahr, P., Graulund, C., M\u00f8gelberg, R.: Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion (2020), https:\/\/arxiv.org\/abs\/2003.03170, To Appear in POPL\u201921"},{"key":"20_CR9","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Berger, U., Matthes, R., Setzer, A.: Martin Hofmann\u2019s Case for Non-Strictly Positive Data Types. In: Dybjer, P., Esp\u00edrito\u00a0Santo, J., Pinto, L. (eds.) 24th International Conference on Types for Proofs and Programs (TYPES 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0130, pp. 1:1\u20131:22. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2018.1, https:\/\/hal.archives-ouvertes.fr\/hal-02365814","DOI":"10.4230\/LIPIcs.TYPES.2018.1"},{"key":"20_CR11","doi-asserted-by":"publisher","unstructured":"Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H.B., Spitters, B., Vezzosi, A.: Guarded cubical type theory. Journal of Automated Reasoning 63(2), 211\u2013253 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9471-7","DOI":"10.1007\/s10817-018-9471-7"},{"key":"20_CR12","doi-asserted-by":"publisher","unstructured":"Birkedal, L., Clouston, R., Mannaa, B., M\u00f8gelberg, R., Pitts, A.M., Spitters, B.: Modal dependent type theory and dependent right adjoints. Mathematical Structures in Computer Science 30(2), 118\u2013138 (2020). https:\/\/doi.org\/10.1017\/S0960129519000197","DOI":"10.1017\/S0960129519000197"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8(4) (2012)","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Bizjak, A., Grathwohl, H.B., Clouston, R., M\u00f8gelberg, R.E., Birkedal, L.: Guarded Dependent Type Theory with Coinductive Types. In: Jacobs, B., L\u00f6ding, C. (eds.) Foundations of Software Science and Computation Structures. pp. 20\u201335. Springer Berlin Heidelberg, Berlin, Heidelberg (2016)","DOI":"10.1007\/978-3-662-49630-5_2"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Bizjak, A., M\u00f8gelberg, R.E.: Denotational semantics for guarded dependent type theory. Mathematical Structures in Computer Science 30(4), 342\u2013378 (2020). https:\/\/doi.org\/10.1017\/S0960129520000080","DOI":"10.1017\/S0960129520000080"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Bradfield, J.C., Walukiewicz, I.: The mu-calculus and Model Checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 871\u2013919. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_26"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair Reactive Programming. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 361\u2013372. POPL \u201914, ACM, New York, NY, USA (2014)","DOI":"10.1145\/2535838.2535881"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Clouston, R., Bizjak, A., Bugge\u00a0Grathwohl, H., Birkedal, L.: The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science 12(3) (2016)","DOI":"10.2168\/LMCS-12(3:7)2016"},{"key":"20_CR19","doi-asserted-by":"publisher","unstructured":"Dreyer, D., Ahmed, A., Birkedal, L.: Logical Step-Indexed Logical Relations. Logical Methods in Computer Science Volume 7, Issue 2 (2011). https:\/\/doi.org\/10.2168\/LMCS-7(2:16)2011, https:\/\/lmcs.episciences.org\/698","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Neis, G., Rossberg, A., Birkedal, L.: A Relational Modal Logic for Higher-order Stateful ADTs. In: Proceedings POPL\u201910. pp. 185\u2013198. ACM (2010)","DOI":"10.1145\/1707801.1706323"},{"key":"20_CR21","doi-asserted-by":"publisher","unstructured":"Elliott, C., Hudak, P.: Functional Reactive Animation. In: Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming. pp. 263\u2013273. ICFP\u201997, ACM, New York, NY, USA (1997). https:\/\/doi.org\/10.1145\/258948.258973, http:\/\/doi.acm.org\/10.1145\/258948.258973","DOI":"10.1145\/258948.258973"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Freeman, T., Pfenning, F.: Refinement Types for ML. In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. pp. 268\u2013277. PLDI\u201991, Association for Computing Machinery, New York, NY, USA (1991). https:\/\/doi.org\/10.1145\/113445.113468, https:\/\/doi.org\/10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"Fujima, K., Ito, S., Kobayashi, N.: Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes. In: APLAS \u201913: Proceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 8301. pp. 17\u201332. Springer-Verlag, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_2, https:\/\/doi.org\/10.1007\/978-3-319-03542-0_2","DOI":"10.1007\/978-3-319-03542-0_2"},{"key":"20_CR24","doi-asserted-by":"publisher","unstructured":"Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. In: Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science. pp. 492\u2013506. LICS \u201920, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3373718.3394736, https:\/\/doi.org\/10.1145\/3373718.3394736","DOI":"10.1145\/3373718.3394736"},{"key":"20_CR25","doi-asserted-by":"publisher","unstructured":"Guatto, A.: A Generalized Modality for Recursion. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. pp. 482\u2013491. LICS \u201918, ACM, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3209108.3209148","DOI":"10.1145\/3209108.3209148"},{"key":"20_CR26","doi-asserted-by":"publisher","unstructured":"Hofmann, M., Chen, W.: Abstract interpretation from b\u00fcchi automata. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS \u201914, Vienna, Austria, July 14 - 18, 2014. pp. 51:1\u201351:10. ACM (2014). https:\/\/doi.org\/10.1145\/2603088.2603127, https:\/\/doi.org\/10.1145\/2603088.2603127","DOI":"10.1145\/2603088.2603127"},{"key":"20_CR27","doi-asserted-by":"publisher","unstructured":"Hofmann, M., Ledent, J.: A cartesian-closed category for higher-order model checking. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005120, https:\/\/doi.org\/10.1109\/LICS.2017.8005120","DOI":"10.1109\/LICS.2017.8005120"},{"key":"20_CR28","unstructured":"Jaber, G., Riba, C.: Temporal Refinements for Guarded Recursive Types (Jan 2021), https:\/\/hal.archives-ouvertes.fr\/hal-02512655, full version. Available on HAL (hal-02512655)"},{"key":"20_CR29","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in logic and the foundations of mathematics, Elsevier (2001)"},{"key":"20_CR30","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study. ITA 35(1), 31\u201359 (2001)","DOI":"10.1051\/ita:2001108"},{"key":"20_CR31","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2016)","DOI":"10.1017\/CBO9781316823187"},{"key":"20_CR32","doi-asserted-by":"publisher","unstructured":"Jeffrey, A.: LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs. In: Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification. pp. 49\u201360. PLPV\u201912, ACM, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2103776.2103783, http:\/\/doi.acm.org\/10.1145\/2103776.2103783","DOI":"10.1145\/2103776.2103783"},{"key":"20_CR33","doi-asserted-by":"publisher","unstructured":"Jeltsch, W.: An Abstract Categorical Semantics for Functional Reactive Programming with Processes. In: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages Meets Program Verification. pp. 47\u201358. PLPV\u201914, ACM, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2541568.2541573, http:\/\/doi.acm.org\/10.1145\/2541568.2541573","DOI":"10.1145\/2541568.2541573"},{"key":"20_CR34","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying functional programs using abstract interpreters. In: International Conference on Computer Aided Verification. pp. 470\u2013485. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_38"},{"key":"20_CR35","unstructured":"Jones, G., Gibbons, J.: Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips. Technical report, University of Auckland (1993)"},{"key":"20_CR36","doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018)","DOI":"10.1017\/S0956796818000151"},{"key":"20_CR37","doi-asserted-by":"publisher","unstructured":"Kobayashi, K., Nishikawa, T., Igarashi, A., Unno, H.: Temporal Verification of Programs via First-Order Fixpoint Logic. In: Chang, B.E. (ed.) Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11822, pp. 413\u2013436. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_20, https:\/\/doi.org\/10.1007\/978-3-030-32304-2_20","DOI":"10.1007\/978-3-030-32304-2_20"},{"key":"20_CR38","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Fedyukovich, G., Gupta, A.: Fold\/Unfold Transformations for Fixpoint Logic. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12079, pp. 195\u2013214. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_12, https:\/\/doi.org\/10.1007\/978-3-030-45237-7_12","DOI":"10.1007\/978-3-030-45237-7_12"},{"key":"20_CR39","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science. pp. 179\u2013188. IEEE (2009)","DOI":"10.1109\/LICS.2009.29"},{"key":"20_CR40","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. SIGPLAN Not. 46(6), 222\u2013233 (2011). https:\/\/doi.org\/10.1145\/1993316.1993525, https:\/\/doi.org\/10.1145\/1993316.1993525","DOI":"10.1145\/1993316.1993525"},{"key":"20_CR41","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Tabuchi, N., Unno, H.: Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification. In: POPL \u201910: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 495\u2013508. Association for Computing Machinery, New York, NY, USA (2010). https:\/\/doi.org\/10.1145\/1707801.1706355, https:\/\/doi.org\/10.1145\/1707801.1706355","DOI":"10.1145\/1707801.1706355"},{"key":"20_CR42","doi-asserted-by":"publisher","unstructured":"Koskinen, E., Terauchi, T.: Local Temporal Reasoning. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS\u201914, Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2603088.2603138, https:\/\/doi.org\/10.1145\/2603088.2603138","DOI":"10.1145\/2603088.2603138"},{"key":"20_CR43","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theoretical Computer Science 27(3), 333 \u2013 354 (1983), special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"20_CR44","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R.: Higher-order functional reactive programming without spacetime leaks. In: Proceedings of ICFP\u201913. pp. 221\u2013232. ACM, New York, NY, USA (2013)","DOI":"10.1145\/2544174.2500588"},{"key":"20_CR45","doi-asserted-by":"publisher","unstructured":"Krishnaswami, N.R., Benton, N.: Ultrametric Semantics of Reactive Programs. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science. pp. 257\u2013266 (2011). https:\/\/doi.org\/10.1109\/LICS.2011.38","DOI":"10.1109\/LICS.2011.38"},{"key":"20_CR46","doi-asserted-by":"crossref","unstructured":"Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic Termination Verification for Higher-Order Functional Programs. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 392\u2013411. ESOP\u201914, Springer Berlin Heidelberg, Berlin, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54833-8_21"},{"key":"20_CR47","unstructured":"Mac\u00a0Lane, S., Moerdijk, I.: Sheaves in geometry and logic: A first introduction to topos theory. Springer (1992)"},{"key":"20_CR48","unstructured":"Marin, S.: Modal proof theory through a focused telescope. Phd thesis, Universit\u00e9 Paris Saclay (Jan 2018), https:\/\/hal.archives-ouvertes.fr\/tel-01951291"},{"key":"20_CR49","doi-asserted-by":"publisher","unstructured":"McBride, C., Paterson, R.: Applicative programming with effects. Journal of Functional Programming 18(1) (2008). https:\/\/doi.org\/10.1017\/S0956796807006326","DOI":"10.1017\/S0956796807006326"},{"key":"20_CR50","doi-asserted-by":"crossref","unstructured":"M\u00f8gelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: Proceedings of CSL-LICS 2014. CSL-LICS \u201914, ACM (2014)","DOI":"10.1145\/2603088.2603132"},{"key":"20_CR51","doi-asserted-by":"publisher","unstructured":"Murase, A., Terauchi, T., Kobayashi, N., Sato, R., Unno, H.: Temporal Verification of Higher-Order Functional Programs. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 57\u201368. POPL\u201916, Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2837614.2837667, https:\/\/doi.org\/10.1145\/2837614.2837667","DOI":"10.1145\/2837614.2837667"},{"key":"20_CR52","unstructured":"Nakano, H.: A Modality for Recursion. In: Proceedings of LICS\u201900. pp. 255\u2013266. IEEE Computer Society (2000)"},{"key":"20_CR53","doi-asserted-by":"publisher","unstructured":"Nanjo, Y., Unno, H., Koskinen, E., Terauchi, T.: A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science. pp. 759\u2013768. LICS\u201918, Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3209108.3209204, https:\/\/doi.org\/10.1145\/3209108.3209204","DOI":"10.1145\/3209108.3209204"},{"key":"20_CR54","unstructured":"Ong, C.H.L.: On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In: Proceedings of LICS 2006. pp. 81\u201390. IEEE Computer Society (2006)"},{"key":"20_CR55","doi-asserted-by":"crossref","unstructured":"Pir\u00f3g, M., Gibbons, J.: The coinductive resumption monad. Electronic Notes in Theoretical Computer Science 308, 273\u2013288 (2014)","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"20_CR56","doi-asserted-by":"crossref","unstructured":"Plotkin, G., Stirling, C.: A Framework for Intuitionistic Modal Logics: Extended Abstract. In: Proceedings of the 1986 Conference on Theoretical Aspects of Reasoning About Knowledge. pp. 399\u2013406. TARK \u201986, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (1986)","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"20_CR57","doi-asserted-by":"publisher","unstructured":"Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid Types. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 159\u2013169. PLDI\u201908, Association for Computing Machinery, New York, NY, USA (2008). https:\/\/doi.org\/10.1145\/1375581.1375602, https:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"20_CR58","doi-asserted-by":"crossref","unstructured":"Santocanale, L., Venema, Y.: Completeness for flat modal fixpoint logics. Ann. Pure Appl. Logic 162(1), 55\u201382 (2010)","DOI":"10.1016\/j.apal.2010.07.003"},{"key":"20_CR59","doi-asserted-by":"publisher","unstructured":"Sato, R., Iwayama, N., Kobayashi, N.: Combining higher-order model checking with refinement type inference. In: Hermenegildo, M.V., Igarashi, A. (eds.) Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019. pp. 47\u201353. ACM (2019). https:\/\/doi.org\/10.1145\/3294032.3294081, https:\/\/doi.org\/10.1145\/3294032.3294081","DOI":"10.1145\/3294032.3294081"},{"key":"20_CR60","unstructured":"Simpson, A.K.: The Proof Theory and Semantics of Intuitionistic Modal Logic. Phd thesis, University of Edinburgh (Jul 1994), https:\/\/www.era.lib.ed.ac.uk\/handle\/1842\/407"},{"key":"20_CR61","doi-asserted-by":"publisher","unstructured":"Skalka, C., Smith, S., Van\u00a0horn, D.: Types and Trace Effects of Higher Order Programs. J. Funct. Program. 18(2), 179\u2013249 (Mar 2008). https:\/\/doi.org\/10.1017\/S0956796807006466, https:\/\/doi.org\/10.1017\/S0956796807006466","DOI":"10.1017\/S0956796807006466"},{"key":"20_CR62","doi-asserted-by":"publisher","unstructured":"Spies, S., Krishnaswami, N., Dreyer, D.: Transfinite Step-Indexing for Termination. Proc. ACM Program. Lang. 5(POPL) (Jan 2021). https:\/\/doi.org\/10.1145\/3434294, https:\/\/doi.org\/10.1145\/3434294","DOI":"10.1145\/3434294"},{"key":"20_CR63","doi-asserted-by":"publisher","unstructured":"Sprenger, C., Dam, M.: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the $$\\mu $$-Calculus. In: Gordon, A.D. (ed.) Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02620, pp. 425\u2013440. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-36576-1_27, https:\/\/doi.org\/10.1007\/3-540-36576-1_27","DOI":"10.1007\/3-540-36576-1_27"},{"key":"20_CR64","doi-asserted-by":"publisher","unstructured":"Unno, H., Satake, Y., Terauchi, T.: Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proc. ACM Program. Lang. 2(POPL), 12:1\u201312:29 (2018). https:\/\/doi.org\/10.1145\/3158100, https:\/\/doi.org\/10.1145\/3158100","DOI":"10.1145\/3158100"},{"key":"20_CR65","unstructured":"Vazou, N.: Liquid Haskell: Haskell as a theorem prover. Ph.D. thesis, UC San Diego (2016)"},{"key":"20_CR66","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement Types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming. pp. 269\u2013282. ICFP\u201914, Association for Computing Machinery, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2628136.2628161, https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"},{"key":"20_CR67","doi-asserted-by":"publisher","unstructured":"Veltri, N., van\u00a0der Weide, N.: Guarded Recursion in Agda via Sized Types. In: Geuvers, H. (ed.) 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0131, pp. 32:1\u201332:19. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2019.32, http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2019\/10539","DOI":"10.4230\/LIPIcs.FSCD.2019.32"},{"key":"20_CR68","doi-asserted-by":"crossref","unstructured":"Walukiewicz, I.: Completeness of Kozen\u2019s Axiomatisation of the Propositional $$\\mu $$-Calculus. Information and Computation 157(1-2), 142\u2013182 (2000)","DOI":"10.1006\/inco.1999.2836"},{"key":"20_CR69","doi-asserted-by":"publisher","unstructured":"Watanabe, K., Tsukada, T., Oshikawa, H., Kobayashi, N.: Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking. In: Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation. pp. 22\u201334. PEPM 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3294032.3294077, https:\/\/doi.org\/10.1145\/3294032.3294077","DOI":"10.1145\/3294032.3294077"},{"key":"20_CR70","doi-asserted-by":"publisher","unstructured":"Xia, L.Y., Zakowski, Y., He, P., Hur, C.K., Malecha, G., Pierce, B.C., Zdancewic, S.: Interaction Trees: Representing Recursive and Impure Programs in Coq. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371119, https:\/\/doi.org\/10.1145\/3371119","DOI":"10.1145\/3371119"}],"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-030-72019-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T04:47:18Z","timestamp":1671684438000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-72019-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720186","9783030720193"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72019-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"79","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":"24","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":"30% - 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-5","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":"10","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)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}