{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T12:51:22Z","timestamp":1726059082062},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030341749"},{"type":"electronic","value":"9783030341756"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-34175-6_8","type":"book-chapter","created":{"date-parts":[[2019,11,17]],"date-time":"2019-11-17T19:01:29Z","timestamp":1574017289000},"page":"136-155","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Type-Based HFL Model Checking Algorithm"],"prefix":"10.1007","author":[{"given":"Youkichi","family":"Hosoi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-540-75560-9_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Axelsson","year":"2007","unstructured":"Axelsson, R., Lange, M.: Model checking the first-order fragment of higher-order fixpoint logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 62\u201376. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75560-9_7"},{"issue":"2:7","key":"8_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-3(2:7)2007","volume":"3","author":"R Axelsson","year":"2007","unstructured":"Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Logical Methods Comput. Sci. 3(2:7), 1\u201333 (2007). https:\/\/doi.org\/10.2168\/LMCS-3(2:7)2007","journal-title":"Logical Methods Comput. Sci."},{"key":"8_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139032636","author":"H Barendregt","year":"2013","unstructured":"Barendregt, H., Statman, R., Dekkers, W.: Lambda Calculus with Types. Cambridge University Press (2013). https:\/\/doi.org\/10.1017\/CBO9781139032636","journal-title":"Cambridge University Press"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Broadbent, C., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of the 22nd EACSL Annual Conference on Computer Science Logic (CSL 2013). LIPIcs, vol. 23, pp. 129\u2013148. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2013). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2013.129","DOI":"10.4230\/LIPIcs.CSL.2013.129"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Hosoi, Y., Kobayashi, N., Tsukada, T.: A type-based HFL model checking algorithm. arXiv e-prints arXiv:1908.10416 (2019)","DOI":"10.1007\/978-3-030-34175-6_8"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290\u2013301. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46541-3_24"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2009), pp. 25\u201336. ACM (2009). https:\/\/doi.org\/10.1145\/1599410.1599415","DOI":"10.1145\/1599410.1599415"},{"key":"8_CR9","unstructured":"Kobayashi, N.: HorSat2: a model checker for HORS based on SATuration (2015). https:\/\/github.com\/hopv\/horsat2"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Kobayashi, N., Lozes, E., Bruse, F.: On the relationship between higher-order recursion schemes and higher-order fixpoint logic. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pp. 246\u2013259. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009854","DOI":"10.1145\/3009837.3009854"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-89884-1_25","volume-title":"Programming Languages and Systems","author":"N Kobayashi","year":"2018","unstructured":"Kobayashi, N., Tsukada, T., Watanabe, K.: Higher-order program verification via HFL model checking. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 711\u2013738. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_25"},{"key":"8_CR12","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1016\/j.tcs.2014.08.020","volume":"560","author":"M Lange","year":"2014","unstructured":"Lange, M., Lozes, \u00c9., Guzm\u00e1n, M.V.: Model-checking process equivalences. Theoret. Comput. Sci. 560, 326\u2013347 (2014). https:\/\/doi.org\/10.1016\/j.tcs.2014.08.020","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR13","unstructured":"Lozes, \u00c9.: Personal communication"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"132","DOI":"10.4204\/EPTCS.191.12","volume":"191","author":"Etienne Lozes","year":"2015","unstructured":"Lozes, \u00c9.: A type-directed negation elimination. In: Proceedings of the 10th International Workshop on Fixed Points in Computer Science (FICS 2015). EPTCS, vol. 191, pp. 132\u2013142 (2015). https:\/\/doi.org\/10.4204\/EPTCS.191.12","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Neatherway, R.P., Ong, C.H.L.: TravMC2: higher-order model checking for alternating parity tree automata. In: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software (SPIN 2014), pp. 129\u2013132. ACM (2014). https:\/\/doi.org\/10.1145\/2632362.2632381","DOI":"10.1145\/2632362.2632381"},{"key":"8_CR16","doi-asserted-by":"publisher","unstructured":"Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pp. 81\u201390. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/LICS.2006.38","DOI":"10.1109\/LICS.2006.38"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Ramsay, S.J., Neatherway, R.P., Ong, C.H.L.: A type-directed abstraction refinement approach to higher-order model checking. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), pp. 61\u201372. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535873","DOI":"10.1145\/2535838.2535873"},{"key":"8_CR18","unstructured":"Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, Carnegie-Mellon University (1991)"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Suzuki, R., Fujima, K., Kobayashi, N., Tsukada, T.: Streett automata model checking of higher-order recursion schemes. In: Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). LIPIcs, vol. 84, pp. 32:1\u201332:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2017.32","DOI":"10.4230\/LIPIcs.FSCD.2017.32"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-540-28644-8_33","volume-title":"CONCUR 2004 - Concurrency Theory","author":"M Viswanathan","year":"2004","unstructured":"Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 512\u2013528. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_33"},{"key":"8_CR21","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 (PEPM 2019), pp. 22\u201334. ACM (2019). https:\/\/doi.org\/10.1145\/3294032.3294077","DOI":"10.1145\/3294032.3294077"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34175-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,12]],"date-time":"2019-12-12T07:17:59Z","timestamp":1576135079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34175-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030341749","9783030341756"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34175-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"18 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nusa Dua, Bali","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Indonesia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}