{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:16:29Z","timestamp":1743102989694,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631387"},{"type":"electronic","value":"9783319631394"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-63139-4_18","type":"book-chapter","created":{"date-parts":[[2017,7,23]],"date-time":"2017-07-23T23:22:55Z","timestamp":1500852175000},"page":"311-327","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Coinductive Soundness of Corecursive Type Class Resolution"],"prefix":"10.1007","author":[{"given":"Franti\u0161ek","family":"Farka","sequence":"first","affiliation":[]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[]},{"given":"Kevin","family":"Hammond","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"key":"18_CR1","unstructured":"Colmerauer, A.: Equations and inequations on finite and infinite trees. In: FGCS, pp. 85\u201399 (1984)"},{"issue":"4\u20135","key":"18_CR2","first-page":"635","volume":"15","author":"E Angelis De","year":"2015","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Proving correctness of imperative programs by linearizing constrained horn clauses. TPLP 15(4\u20135), 635\u2013650 (2015)","journal-title":"TPLP"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Devriese, D., Piessens, F.: On the bright side of type classes: instance arguments in Agda. In: Proceedings of ICFP 2011, Tokyo, 19\u201321 September 2011, pp. 143\u2013155 (2011)","DOI":"10.1145\/2034574.2034796"},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Fu, P., Komendantskaya, E.: Operational semantics of resolution and productivity in Horn clause logic. Form. Asp. Comput. 29, 453\u2013474 (2017). doi:\n                      10.1007\/s00165-016-0403-1","DOI":"10.1007\/s00165-016-0403-1"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-29604-3_9","volume-title":"Functional and Logic Programming","author":"P Fu","year":"2016","unstructured":"Fu, P., Komendantskaya, E., Schrijvers, T., Pond, A.: Proof relevant corecursive resolution. In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 126\u2013143. Springer, Cham (2016). doi:\n                      10.1007\/978-3-319-29604-3_9"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. In: Proceedings of ICFP 2011, Tokyo, 19\u201321 September 2011, pp. 163\u2013175 (2011)","DOI":"10.1145\/2034574.2034798"},{"issue":"2","key":"18_CR7","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/227699.227700","volume":"18","author":"CV Hall","year":"1996","unstructured":"Hall, C.V., Hammond, K., Jones, S.L.P., Wadler, P.: Type classes in Haskell. ACM Trans. Program. Lang. Syst. 18(2), 109\u2013138 (1996)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR8","unstructured":"Howard, W.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pp. 479\u2013490. Academic Press, New York (1980)"},{"issue":"3","key":"18_CR9","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0304-3975(86)90027-7","volume":"46","author":"J Jaffar","year":"1986","unstructured":"Jaffar, J., Stuckey, P.J.: Semantics of infinite tree logic programming. Theor. Comput. Sci. 46(3), 141\u2013158 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR10","unstructured":"Komendantskaya, E., Li T.: Productive corecursion in logic programming. In: Proceedings of ICLP 2017. TPLP (to appear, 2017)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"L\u00e4mmel, R., Peyton Jones, S.L.: Scrap your boilerplate with class: extensible generic functions. In: Proceedings of ICFP 2005, Tallinn, 26\u201328 September 2005, pp. 204\u2013215 (2005)","DOI":"10.1145\/1090189.1086391"},{"key":"18_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-83189-8","volume-title":"Foundations of Logic Programming","author":"JW Lloyd","year":"1987","unstructured":"Lloyd, J.W.: Foundations of Logic Programming, 2nd edn. Springer, Heidelberg (1987)","edition":"2"},{"issue":"4","key":"18_CR13","doi-asserted-by":"publisher","first-page":"15:1","DOI":"10.1145\/1516507.1516510","volume":"31","author":"D Sangiorgi","year":"2009","unstructured":"Sangiorgi, D.: On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst. 31(4), 15:1\u201315:41 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-540-73420-8_42","volume-title":"Automata, Languages and Programming","author":"L Simon","year":"2007","unstructured":"Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: extending logic programming with coinduction. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 472\u2013483. Springer, Heidelberg (2007). doi:\n                      10.1007\/978-3-540-73420-8_42"},{"issue":"6","key":"18_CR15","doi-asserted-by":"publisher","first-page":"1216","DOI":"10.1145\/1108970.1108974","volume":"27","author":"PJ Stuckey","year":"2005","unstructured":"Stuckey, P.J., Sulzmann, M.: A theory of overloading. ACM Trans. Program. Lang. Syst. 27(6), 1216\u20131269 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of POPL 1989, pp. 60\u201376. ACM, New York (1989)","DOI":"10.1145\/75277.75283"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63139-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:52:11Z","timestamp":1558320731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63139-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631387","9783319631394"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63139-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"25 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Edinburgh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 September 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 September 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.cliplab.org\/Conferences\/LOPSTR16\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}