{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T23:11:23Z","timestamp":1765667483886,"version":"3.41.0"},"publisher-location":"Singapore","reference-count":37,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819789429"},{"type":"electronic","value":"9789819789436"}],"license":[{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T00:00:00Z","timestamp":1730073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-981-97-8943-6_6","type":"book-chapter","created":{"date-parts":[[2024,10,28]],"date-time":"2024-10-28T08:45:29Z","timestamp":1730105129000},"page":"109-129","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4953-8202","authenticated-orcid":false,"given":"Michael","family":"Hanus","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,10,28]]},"reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1016\/j.jsc.2004.01.001","volume":"40","author":"E Albert","year":"2005","unstructured":"Albert, E., Hanus, M., Huch, F., Oliver, J., Vidal, G.: Operational semantics for declarative multi-paradigm languages. J. Symb. Comput. 40(1), 795\u2013829 (2005). https:\/\/doi.org\/10.1016\/j.jsc.2004.01.001","journal-title":"J. Symb. Comput."},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Antoy, S.: Constructor-based conditional narrowing. In: Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), pp. 199\u2013206. ACM Press (2001).https:\/\/doi.org\/10.1145\/773184.773205","DOI":"10.1145\/773184.773205"},{"issue":"4","key":"6_CR3","doi-asserted-by":"publisher","first-page":"776","DOI":"10.1145\/347476.347484","volume":"47","author":"S Antoy","year":"2000","unstructured":"Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776\u2013822 (2000). https:\/\/doi.org\/10.1145\/347476.347484","journal-title":"J. ACM"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Antoy, S., Hanus, M.: Functional logic design patterns. In: Proceedings of the 6th International Symposium on Functional and Logic Programming (FLOPS 2002), pp. 67\u201387. Springer LNCS 2441 (2002)https:\/\/doi.org\/10.1007\/3-540-45788-7_4","DOI":"10.1007\/3-540-45788-7_4"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Antoy, S., Hanus, M.: Set functions for functional logic programming. In: Proceedings of the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP\u201909), pp. 73\u201382. ACM Press (2009). https:\/\/doi.org\/10.1145\/1599410.1599420","DOI":"10.1145\/1599410.1599420"},{"issue":"4","key":"6_CR6","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1721654.1721675","volume":"53","author":"S Antoy","year":"2010","unstructured":"Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM 53(4), 74\u201385 (2010). https:\/\/doi.org\/10.1145\/1721654.1721675","journal-title":"Commun. ACM"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Antoy, S., Hanus, M.: Contracts and specifications for functional logic programming. In: Proceedings of the 14th International Symposium on Practical Aspects of Declarative Languages (PADL 2012), pp. 33\u201347. Springer LNCS 7149 (2012). https:\/\/doi.org\/10.1007\/978-3-642-27694-1_4","DOI":"10.1007\/978-3-642-27694-1_4"},{"key":"6_CR8","doi-asserted-by":"publisher","unstructured":"Antoy, S., Hanus, M., Jost, A., Libby, S.: ICurry. In: Declarative Programming and Knowledge Management\u2014Conference on Declarative Programming (DECLARE 2019), pp. 286\u2013307. Springer LNCS 12057 (2020). https:\/\/doi.org\/10.1007\/978-3-030-46714-2_18","DOI":"10.1007\/978-3-030-46714-2_18"},{"key":"6_CR9","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"5","key":"6_CR10","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013). https:\/\/doi.org\/10.1017\/S095679681300018X","journal-title":"J. Funct. Program."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Bra\u00dfel, B., Hanus, M., Huch, F.: Encapsulating non-determinism in functional logic computations. J. Funct. Logic Program. 2004(6) (2004)","DOI":"10.1007\/978-3-540-24836-1_14"},{"key":"6_CR12","doi-asserted-by":"publisher","unstructured":"Bueno, F., L\u00f3pez-Garc\u00eda, P., Hermenegildo, M.: Multivariant non-failure analysis via standard abstract interpretation. In: 7th International Symposium on Functional and Logic Programming (FLOPS 2004). pp. 100\u2013116. Springer LNCS 2998 (2004). https:\/\/doi.org\/10.1007\/978-3-540-24754-8_9","DOI":"10.1007\/978-3-540-24754-8_9"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Debray, S., L\u00f3pez-Garc\u00eda, P., Hermenegildo, M.: Non-failure analysis for logic programs. In: 14th International Conference on Logic Programming (ICLP\u201997), pp. 48\u201362. MIT Press (1997)","DOI":"10.7551\/mitpress\/4299.003.0010"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0743-1066(98)10029-8","volume":"40","author":"J Gonz\u00e1lez-Moreno","year":"1999","unstructured":"Gonz\u00e1lez-Moreno, J., Hortal\u00e1-Gonz\u00e1lez, M., L\u00f3pez-Fraguas, F., Rodr\u00edguez-Artalejo, M.: An approach to declarative programming based on a rewriting logic. J. Log. Program. 40, 47\u201387 (1999). https:\/\/doi.org\/10.1016\/S0743-1066(98)10029-8","journal-title":"J. Log. Program."},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Hanus, M.: Functional logic programming: from theory to curry. In: Programming Logics - Essays in Memory of Harald Ganzinger, pp. 123\u2013168. Springer LNCS 7797 (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_6","DOI":"10.1007\/978-3-642-37651-1_6"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Hanus, M.: Verifying fail-free declarative programs. In: Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018), pp. 12:1\u201312:13. ACM Press (2018). https:\/\/doi.org\/10.1145\/3236950.3236957","DOI":"10.1145\/3236950.3236957"},{"issue":"4","key":"6_CR17","doi-asserted-by":"publisher","first-page":"538","DOI":"10.1017\/S1471068422000187","volume":"22","author":"M Hanus","year":"2022","unstructured":"Hanus, M.: From logic to functional logic programs. Theory Pract. Logic Program. 22(4), 538\u2013554 (2022). https:\/\/doi.org\/10.1017\/S1471068422000187","journal-title":"Theory Pract. Logic Program."},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Hanus, M.: Inferring non-failure conditions for declarative programs. In: Proceedings of the 17th International Symposium on Functional and Logic Programming (FLOPS 2024), pp. 167\u2013187. Springer LNCS 14659 (2024). https:\/\/doi.org\/10.1007\/978-981-97-2300-3_10","DOI":"10.1007\/978-981-97-2300-3_10"},{"key":"6_CR19","unstructured":"Hanus, M. (ed.): Curry: an integrated functional logic language (vers. 0.9.0). Available at http:\/\/www.curry-lang.org (2016)"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: verifying functional programs using abstract interpreters. In: 23rd International Conference on Computer Aided Verification (CAV 2011). pp. 470\u2013485. Springer LNCS 6806 (2011).https:\/\/doi.org\/10.1007\/978-3-642-22110-1_38","DOI":"10.1007\/978-3-642-22110-1_38"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Lindahl, T., Sagonas, K.: Practical type inference based on success typings. In: Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2006). pp. 167\u2013178. ACM Press (2006). https:\/\/doi.org\/10.1145\/1140335.1140356","DOI":"10.1145\/1140335.1140356"},{"issue":"1","key":"6_CR22","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1017\/S1471068403001728","volume":"4","author":"F L\u00f3pez-Fraguas","year":"2004","unstructured":"L\u00f3pez-Fraguas, F., S\u00e1nchez-Hern\u00e1ndez, J.: A proof theoretic approach to failure in functional logic programming. Theory Pract. Logic Program. 4(1), 41\u201374 (2004). https:\/\/doi.org\/10.1017\/S1471068403001728","journal-title":"Theory Pract. Logic Program."},{"key":"6_CR23","doi-asserted-by":"publisher","unstructured":"Lux, W.: Implementing encapsulated search for a lazy functional logic language. In: Proceedings of 4th Fuji International Symposium on Functional and Logic Programming (FLOPS\u201999), pp. 100\u2013113. Springer LNCS 1722 (1999). https:\/\/doi.org\/10.1007\/10705424_7","DOI":"10.1007\/10705424_7"},{"key":"6_CR24","unstructured":"Meyer, B.: Object-oriented Software Construction, 2nd edn. Prentice Hall (1997)"},{"issue":"5","key":"6_CR25","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/3057284","volume":"60","author":"B Meyer","year":"2017","unstructured":"Meyer, B.: Ending null pointer crashes. Commun. ACM 60(5), 8\u20139 (2017). https:\/\/doi.org\/10.1145\/3057284","journal-title":"Commun. ACM"},{"key":"6_CR26","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR27","unstructured":"Mitchell, N., Runciman, C.: A static checker for safe pattern matching in Haskell. In: Trends in Functional Programming, vol.\u00a06, pp. 15\u201330. Intellect (2007)"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Mitchell, N., Runciman, C.: Not all patterns, but enough: an automatic verifier for partial but sufficient pattern matching. In: Proceedings of the 1st ACM SIGPLAN Symposium on Haskell (Haskell 2008), pp. 49\u201360. ACM (2008). https:\/\/doi.org\/10.1145\/1411286.1411293","DOI":"10.1145\/1411286.1411293"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008). pp. 337\u2013340. Springer LNCS 4963 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3","DOI":"10.1007\/978-3-540-78800-3"},{"key":"6_CR30","doi-asserted-by":"publisher","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Proceedings of the 6th International School on Advanced Functional Programming (AFP\u201908). pp. 230\u2013266. Springer LNCS 5832 (2008). https:\/\/doi.org\/10.1007\/978-3-642-04652-0_5","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"6_CR31","unstructured":"Peyton\u00a0Jones, S. (ed.): Haskell 98 Language and Libraries\u2014The Revised Report. Cambridge University Press (2003)"},{"key":"6_CR32","doi-asserted-by":"publisher","unstructured":"Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI\u201908). pp. 159\u2013169. ACM Press (2008). https:\/\/doi.org\/10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"6_CR33","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0304-3975(84)90119-1","volume":"34","author":"T Sato","year":"1984","unstructured":"Sato, T., Tamaki, H.: Enumeration of success patterns in logic programs. Theoret. Comput. Sci. 34, 227\u2013240 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90119-1","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR34","doi-asserted-by":"publisher","unstructured":"Stump, A.: Verified Functional Programming in Agda. ACM and Morgan & Claypool (2016). https:\/\/doi.org\/10.1145\/2841316","DOI":"10.1145\/2841316"},{"key":"6_CR35","doi-asserted-by":"publisher","unstructured":"Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Proceedings of the 11th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP\u201909). pp. 277\u2013288. ACM Press (2009). https:\/\/doi.org\/10.1145\/1599410.1599445","DOI":"10.1145\/1599410.1599445"},{"key":"6_CR36","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E., Jhala, R.: LiquidHaskell: experience with refinement types in the real world. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, pp. 39\u201351. ACM Press (2014).https:\/\/doi.org\/10.1145\/2633357.2633366","DOI":"10.1145\/2633357.2633366"},{"key":"6_CR37","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E., Jhala, R., Vytiniotis, D., Peyton\u00a0Jones, S.: Refinement types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP). pp. 269\u2013282. ACM Press (2014). https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"}],"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-981-97-8943-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T16:52:37Z","timestamp":1748364757000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-97-8943-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,28]]},"ISBN":["9789819789429","9789819789436"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-981-97-8943-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,28]]},"assertion":[{"value":"28 October 2024","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":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}