{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T02:46:16Z","timestamp":1776393976861,"version":"3.51.2"},"publisher-location":"Cham","reference-count":77,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171834","type":"print"},{"value":"9783030171841","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17184-1_28","type":"book-chapter","created":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T17:34:04Z","timestamp":1554572044000},"page":"783-813","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses"],"prefix":"10.1007","author":[{"given":"Henning","family":"Basold","sequence":"first","affiliation":[]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[]},{"given":"Yue","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,6]]},"reference":[{"issue":"1","key":"28_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.tcs.2005.06.002","volume":"342","author":"M Abbott","year":"2005","unstructured":"Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. TCS 342(1), 3\u201327 (2005). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2005.06.002","journal-title":"TCS"},{"key":"28_CR2","doi-asserted-by":"publisher","unstructured":"Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: POPL 2013, pp. 27\u201338 (2013). \n                      https:\/\/doi.org\/10.1145\/2429069.2429075","DOI":"10.1145\/2429069.2429075"},{"key":"28_CR3","unstructured":"Aczel, P.: Non-well-founded sets. Center for the Study of Language and Information, Stanford University (1988)"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-47797-7_3","volume-title":"Algebraic and Coalgebraic Methods in the Mathematics of Program Construction","author":"P Aczel","year":"2002","unstructured":"Aczel, P.: Algebras and coalgebras. In: Backhouse, R., Crole, R., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, pp. 79\u201388. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-47797-7_3"},{"issue":"1\u20133","key":"28_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(02)00728-4","volume":"300","author":"P Aczel","year":"2003","unstructured":"Aczel, P., Ad\u00e1mek, J., Milius, S., Velebil, J.: Infinite trees and completely iterative theories: a coalgebraic view. TCS 300(1\u20133), 1\u201345 (2003). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(02)00728-4","journal-title":"TCS"},{"issue":"1\/2","key":"28_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(01)00240-7","volume":"294","author":"J Ad\u00e1mek","year":"2003","unstructured":"Ad\u00e1mek, J.: On final coalgebras of continuous functors. Theor. Comput. Sci. 294(1\/2), 3\u201329 (2003). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(01)00240-7","journal-title":"Theor. Comput. Sci."},{"key":"28_CR7","unstructured":"P.L. group on Agda: Agda Documentation. Technical report, Chalmers and Gothenburg University (2015). \n                      http:\/\/wiki.portal.chalmers.se\/agda\/\n                      \n                    , version 2.4.2.5"},{"key":"28_CR8","doi-asserted-by":"publisher","unstructured":"Appel, A.W., Melli\u00e8s, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL, pp. 109\u2013122. ACM (2007). \n                      https:\/\/doi.org\/10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: ICFP, pp. 197\u2013208. ACM (2013). \n                      https:\/\/doi.org\/10.1145\/2500365.2500597","DOI":"10.1145\/2500365.2500597"},{"issue":"2","key":"28_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/4650","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., et al.: Abella: a system for reasoning about relational specifications. J. Formaliz. Reason. 7(2), 1\u201389 (2014). \n                      https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"J. Formaliz. Reason."},{"key":"28_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139032636","volume-title":"Lambda Calculus with Types","author":"H Barendregt","year":"2013","unstructured":"Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press, Cambridge (2013)"},{"key":"28_CR12","series-title":"Prentice Hall International Series in Computer Science","volume-title":"Category Theory for Computing Science","author":"M Barr","year":"1995","unstructured":"Barr, M., Wells, C.: Category Theory for Computing Science. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Upper Saddle River (1995). \n                      http:\/\/www.tac.mta.ca\/tac\/reprints\/articles\/22\/tr22abs.html","edition":"2"},{"key":"28_CR13","unstructured":"Basold, H.: Mixed inductive-coinductive reasoning: types, programs and logic. Ph.D. thesis, Radboud University Nijmegen (2018). \n                      http:\/\/hdl.handle.net\/2066\/190323"},{"key":"28_CR14","unstructured":"Basold, H.: Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations. ArXiv e-prints, February 2018. \n                      https:\/\/arxiv.org\/abs\/1802.07143"},{"key":"28_CR15","unstructured":"Basold, H., Komendantskaya, E., Li, Y.: Coinduction in uniform: foundations for corecursive proof search with horn clauses. Extended version of this paper. CoRR abs\/1811.07644 (2018). \n                      http:\/\/arxiv.org\/abs\/1811.07644"},{"issue":"1\u20132","key":"28_CR16","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/S0304-3975(98)00305-3","volume":"224","author":"LD Beklemishev","year":"1999","unstructured":"Beklemishev, L.D.: Parameter free induction and provably total computable functions. TCS 224(1\u20132), 13\u201333 (1999). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(98)00305-3","journal-title":"TCS"},{"issue":"1","key":"28_CR17","doi-asserted-by":"publisher","first-page":"10","DOI":"10.2307\/2273784","volume":"50","author":"J B\u00e9nabou","year":"1985","unstructured":"B\u00e9nabou, J.: Fibered categories and the foundations of naive category theory. J. Symb. Logic 50(1), 10\u201337 (1985). \n                      https:\/\/doi.org\/10.2307\/2273784","journal-title":"J. Symb. Logic"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-662-54458-7_18","volume-title":"Foundations of Software Science and Computation Structures","author":"S Berardi","year":"2017","unstructured":"Berardi, S., Tatsuta, M.: Classical system of Martin-L\u00f6f\u2019s inductive definitions is not equivalent to cyclic proof system. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 301\u2013317. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54458-7_18"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"Birkedal, L., M\u00f8gelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS, pp. 213\u2013222. IEEE Computer Society (2013). \n                      https:\/\/doi.org\/10.1109\/LICS.2013.27","DOI":"10.1109\/LICS.2013.27"},{"key":"28_CR20","doi-asserted-by":"publisher","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. In: Proceedings of LICS 2011, pp. 55\u201364. IEEE Computer Society (2011). \n                      https:\/\/doi.org\/10.1109\/LICS.2011.16","DOI":"10.1109\/LICS.2011.16"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-662-49630-5_2","volume-title":"Foundations of Software Science and Computation Structures","author":"A Bizjak","year":"2016","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.) FoSSaCS 2016. LNCS, vol. 9634, pp. 20\u201335. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49630-5_2\n                      \n                    . \n                      https:\/\/arxiv.org\/abs\/1601.01586"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"28_CR23","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for Higher-Order Logic. In: LICS 2017, pp. 1\u201312. IEEE Computer Society (2017). \n                      https:\/\/doi.org\/10.1109\/LICS.2017.8005071","DOI":"10.1109\/LICS.2017.8005071"},{"key":"28_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-319-94205-6_25","volume-title":"Automated Reasoning","author":"JC Blanchette","year":"2018","unstructured":"Blanchette, J.C., Peltier, N., Robillard, S.: Superposition with datatypes and codatatypes. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 370\u2013387. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-94205-6_25"},{"key":"28_CR25","series-title":"Basic Category Theory","volume-title":"Handbook of Categorical Algebra","author":"F Borceux","year":"2008","unstructured":"Borceux, F.: Handbook of Categorical Algebra. Basic Category Theory, vol. 1. Cambridge University Press, Cambridge (2008)"},{"key":"28_CR26","doi-asserted-by":"publisher","unstructured":"Bottu, G., Karachalias, G., Schrijvers, T., Oliveira, B.C.D.S., Wadler, P.: Quantified class constraints. In: Haskell Symposium, pp. 148\u2013161. ACM (2017). \n                      https:\/\/doi.org\/10.1145\/3122955.3122967","DOI":"10.1145\/3122955.3122967"},{"issue":"6","key":"28_CR27","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1093\/logcom\/exq052","volume":"21","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Simpson, A.: Sequent calculi for induction and infinite descent. J. Log. Comput. 21(6), 1177\u20131216 (2011). \n                      https:\/\/doi.org\/10.1093\/logcom\/exq052","journal-title":"J. Log. Comput."},{"issue":"POPL","key":"28_CR28","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/3158099","volume":"2","author":"TC Burn","year":"2018","unstructured":"Burn, T.C., Ong, C.L., Ramsay, S.J.: Higher-order constrained horn clauses for verification. PACMPL 2(POPL), 11:1\u201311:28 (2018). \n                      https:\/\/doi.org\/10.1145\/3158099","journal-title":"PACMPL"},{"key":"28_CR29","doi-asserted-by":"publisher","unstructured":"Capretta, V.: General Recursion via Coinductive Types. Log. Methods Comput. Sci. 1(2), July 2005. \n                      https:\/\/doi.org\/10.2168\/LMCS-1(2:1)2005","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"28_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-662-46678-0_9","volume-title":"Foundations of Software Science and Computation Structures","author":"R Clouston","year":"2015","unstructured":"Clouston, R., Gor\u00e9, R.: Sequent calculus in the topos of trees. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 133\u2013147. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46678-0_9"},{"key":"28_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for Proofs and Programs","author":"T Coquand","year":"1994","unstructured":"Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62\u201378. Springer, Heidelberg (1994). \n                      https:\/\/doi.org\/10.1007\/3-540-58085-9_72"},{"issue":"1","key":"28_CR32","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"P Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Constructive versions of Tarski\u2019s fixed point theorems. Pac. J. Math. 82(1), 43\u201357 (1979). \n                      http:\/\/projecteuclid.org\/euclid.pjm\/1102785059","journal-title":"Pac. J. Math."},{"key":"28_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/11944836_26","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"C Dax","year":"2006","unstructured":"Dax, C., Hofmann, M., Lange, M.: A proof system for the linear time \n                      \n                        \n                      \n                      $${\\mu }$$\n                    -calculus. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 273\u2013284. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11944836_26"},{"key":"28_CR34","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"M Emden van","year":"1976","unstructured":"van Emden, M., Kowalski, R.: The semantics of predicate logic as a programming language. J. Assoc. Comput. Mach. 23, 733\u2013742 (1976). \n                      https:\/\/doi.org\/10.1145\/321978.321991","journal-title":"J. Assoc. Comput. Mach."},{"key":"28_CR35","doi-asserted-by":"publisher","unstructured":"Endrullis, J., Hansen, H.H., Hendriks, D., Polonsky, A., Silva, A.: A coinductive framework for infinitary rewriting and equational reasoning. In: RTA 2015, pp. 143\u2013159 (2015). \n                      https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2015.143","DOI":"10.4230\/LIPIcs.RTA.2015.143"},{"key":"28_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-63139-4_18","volume-title":"Logic-Based Program Synthesis and Transformation","author":"F Farka","year":"2017","unstructured":"Farka, F., Komendantskaya, E., Hammond, K.: Coinductive soundness of corecursive type class resolution. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 311\u2013327. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63139-4_18"},{"key":"28_CR37","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-29604-3_9"},{"issue":"1","key":"28_CR38","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1017\/S0305004112000394","volume":"154","author":"N Gambino","year":"2013","unstructured":"Gambino, N., Kock, J.: Polynomial functors and polynomial monads. Math. Proc. Cambridge Phil. Soc. 154(1), 153\u2013192 (2013). \n                      https:\/\/doi.org\/10.1017\/S0305004112000394","journal-title":"Math. Proc. Cambridge Phil. Soc."},{"issue":"1","key":"28_CR39","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3\u201331 (2017). \n                      https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"J. Autom. Reason."},{"key":"28_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Automata, Languages and Programming","author":"E Gim\u00e9nez","year":"1998","unstructured":"Gim\u00e9nez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397\u2013408. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/BFb0055070"},{"key":"28_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-74610-2_4","volume-title":"Logic Programming","author":"G Gupta","year":"2007","unstructured":"Gupta, G., Bansal, A., Min, R., Simon, L., Mallya, A.: Coinductive logic programming and its applications. In: Dahl, V., Niemel\u00e4, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 27\u201344. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-74610-2_4"},{"key":"28_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/3-540-18508-9_24","volume-title":"Category Theory and Computer Science","author":"T Hagino","year":"1987","unstructured":"Hagino, T.: A typed lambda calculus with categorical type constructors. In: Pitt, D.H., Poign\u00e9, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 283, pp. 140\u2013157. Springer, Heidelberg (1987). \n                      https:\/\/doi.org\/10.1007\/3-540-18508-9_24"},{"key":"28_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-662-48288-9_12","volume-title":"Static Analysis","author":"K Hashimoto","year":"2015","unstructured":"Hashimoto, K., Unno, H.: Refinement type inference via horn constraint optimization. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 199\u2013216. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-48288-9_12"},{"key":"28_CR44","doi-asserted-by":"publisher","unstructured":"Howard, B.T.: Inductive, coinductive, and pointed types. In: Harper, R., Wexelblat, R.L. (eds.) Proceedings of ICFP 1996, pp. 102\u2013109. ACM (1996). \n                      https:\/\/doi.org\/10.1145\/232627.232640","DOI":"10.1145\/232627.232640"},{"key":"28_CR45","doi-asserted-by":"publisher","unstructured":"Hur, C.K., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: Proceedings of POPL 2013, pp. 193\u2013206. ACM (2013). \n                      https:\/\/doi.org\/10.1145\/2429069.2429093","DOI":"10.1145\/2429069.2429093"},{"key":"28_CR46","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Categorical Logic and Type Theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Amsterdam (1999)"},{"key":"28_CR47","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187","volume-title":"Introduction to Coalgebra: Towards Mathematics of States and Observation","author":"B Jacobs","year":"2016","unstructured":"Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press, Cambridge (2016). \n                      https:\/\/doi.org\/10.1017\/CBO9781316823187\n                      \n                    . \n                      http:\/\/www.cs.ru.nl\/B.Jacobs\/CLG\/JacobsCoalgebraIntro.pdf"},{"issue":"5\u20136","key":"28_CR48","doi-asserted-by":"publisher","first-page":"906","DOI":"10.1017\/S147106841700028X","volume":"17","author":"E Komendantskaya","year":"2017","unstructured":"Komendantskaya, E., Li, Y.: Productive corecursion in logic programming. J. TPLP (ICLP 2017 post-proc.) 17(5\u20136), 906\u2013923 (2017). \n                      https:\/\/doi.org\/10.1017\/S147106841700028X","journal-title":"J. TPLP (ICLP 2017 post-proc.)"},{"key":"28_CR49","doi-asserted-by":"publisher","unstructured":"Komendantskaya, E., Li, Y.: Towards coinductive theory exploration in horn clause logic: Position paper. In: Kahsai, T., Vidal, G. (eds.) Proceedings 5th Workshop on Horn Clauses for Verification and Synthesis, HCVS 2018, Oxford, UK, 13th July 2018, vol. 278, pp. 27\u201333 (2018). \n                      https:\/\/doi.org\/10.4204\/EPTCS.278.5","DOI":"10.4204\/EPTCS.278.5"},{"key":"28_CR50","volume-title":"Introduction to Higher-Order Categorical Logic","author":"J Lambek","year":"1988","unstructured":"Lambek, J., Scott, P.J.: Introduction to Higher-Order Categorical Logic. Cambridge University Press, Cambridge (1988)"},{"key":"28_CR51","doi-asserted-by":"publisher","unstructured":"L\u00e4mmel, R., Peyton Jones, S.L.: Scrap your boilerplate with class: extensible generic functions. In: ICFP 2005, pp. 204\u2013215. ACM (2005). \n                      https:\/\/doi.org\/10.1145\/1086365.1086391","DOI":"10.1145\/1086365.1086391"},{"key":"28_CR52","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-83189-8","edition":"2"},{"key":"28_CR53","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-order logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-order logic. Cambridge University Press, Cambridge (2012)"},{"issue":"1\u20132","key":"28_CR54","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51(1\u20132), 125\u2013157 (1991). \n                      https:\/\/doi.org\/10.1016\/0168-0072(91)90068-W","journal-title":"Ann. Pure Appl. Logic"},{"issue":"3","key":"28_CR55","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(3), 348\u2013375 (1978). \n                      https:\/\/doi.org\/10.1016\/0022-0000(78)90014-4","journal-title":"J. Comput. Syst. Sci."},{"key":"28_CR56","doi-asserted-by":"publisher","unstructured":"M\u00f8gelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: CSL-LICS, pp. 71:1\u201371:10. ACM (2014). \n                      https:\/\/doi.org\/10.1145\/2603088.2603132","DOI":"10.1145\/2603088.2603132"},{"key":"28_CR57","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"Automated Deduction \u2014 CADE-16","author":"G Nadathur","year":"1999","unstructured":"Nadathur, G., Mitchell, D.J.: System description: Teyjus\u2014a compiler and abstract machine based implementation of \n                      \n                        \n                      \n                      $$\\lambda $$\n                    Prolog. CADE-16. LNCS (LNAI), vol. 1632, pp. 287\u2013291. Springer, Heidelberg (1999). \n                      https:\/\/doi.org\/10.1007\/3-540-48660-7_25"},{"key":"28_CR58","doi-asserted-by":"publisher","unstructured":"Nakano, H.: A modality for recursion. In: LICS, pp. 255\u2013266. IEEE Computer Society (2000). \n                      https:\/\/doi.org\/10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"issue":"1&2","key":"28_CR59","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(95)00136-0","volume":"163","author":"D Niwinski","year":"1996","unstructured":"Niwinski, D., Walukiewicz, I.: Games for the \n                      \n                        \n                      \n                      $$\\mu $$\n                    -Calculus. TCS 163(1&2), 99\u2013116 (1996). \n                      https:\/\/doi.org\/10.1016\/0304-3975(95)00136-0","journal-title":"TCS"},{"key":"28_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). \n                      https:\/\/doi.org\/10.1007\/BFb0017309"},{"issue":"3","key":"28_CR61","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"GD Plotkin","year":"1977","unstructured":"Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223\u2013255 (1977). \n                      https:\/\/doi.org\/10.1016\/0304-3975(77)90044-5","journal-title":"Theor. Comput. Sci."},{"key":"28_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"key":"28_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-03741-2_10","volume-title":"Algebra and Coalgebra in Computer Science","author":"G Ro\u015fu","year":"2009","unstructured":"Ro\u015fu, G., Lucanu, D.: Circular coinduction: a proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127\u2013144. Springer, Heidelberg (2009). \n                      https:\/\/doi.org\/10.1007\/978-3-642-03741-2_10"},{"issue":"1","key":"28_CR64","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. TCS 249(1), 3\u201380 (2000). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","journal-title":"TCS"},{"key":"28_CR65","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588","volume-title":"Introduction to Bisimulation and Coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2011)"},{"key":"28_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-45931-6_25","volume-title":"Foundations of Software Science and Computation Structures","author":"L Santocanale","year":"2002","unstructured":"Santocanale, L.: A calculus of circular proofs and its categorical semantics. In: Nielsen, M., Engberg, U. (eds.) FoSSaCS 2002. LNCS, vol. 2303, pp. 357\u2013371. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45931-6_25"},{"issue":"2","key":"28_CR67","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1051\/ita:2002010","volume":"36","author":"L Santocanale","year":"2002","unstructured":"Santocanale, L.: \n                      \n                        \n                      \n                      $$\\mu $$\n                    -bicomplete categories and parity games. RAIRO - ITA 36(2), 195\u2013227 (2002). \n                      https:\/\/doi.org\/10.1051\/ita:2002010","journal-title":"RAIRO - ITA"},{"issue":"3","key":"28_CR68","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1134\/S0001434614090326","volume":"96","author":"DS Shamkanov","year":"2014","unstructured":"Shamkanov, D.S.: Circular proofs for the G\u00f6del-L\u00f6b provability logic. Math. Notes 96(3), 575\u2013585 (2014). \n                      https:\/\/doi.org\/10.1134\/S0001434614090326","journal-title":"Math. Notes"},{"key":"28_CR69","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-73420-8_42"},{"key":"28_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-662-54458-7_17","volume-title":"Foundations of Software Science and Computation Structures","author":"A Simpson","year":"2017","unstructured":"Simpson, A.: Cyclic arithmetic is equivalent to Peano arithmetic. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 283\u2013300. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54458-7_17"},{"key":"28_CR71","series-title":"Universitext","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8601-8","volume-title":"Self-Reference and Modal Logic","author":"C Smory\u0144ski","year":"1985","unstructured":"Smory\u0144ski, C.: Self-Reference and Modal Logic. Universitext. Springer, New York (1985). \n                      https:\/\/doi.org\/10.1007\/978-1-4613-8601-8"},{"issue":"3","key":"28_CR72","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF02757006","volume":"25","author":"RM Solovay","year":"1976","unstructured":"Solovay, R.M.: Provability interpretations of modal logic. Israel J. Math. 25(3), 287\u2013304 (1976). \n                      https:\/\/doi.org\/10.1007\/BF02757006","journal-title":"Israel J. Math."},{"issue":"2","key":"28_CR73","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1017\/S0956796807006569","volume":"18","author":"M Sulzmann","year":"2008","unstructured":"Sulzmann, M., Stuckey, P.J.: HM(X) type inference is CLP(X) solving. J. Funct. Program. 18(2), 251\u2013283 (2008). \n                      https:\/\/doi.org\/10.1017\/S0956796807006569","journal-title":"J. Funct. Program."},{"key":"28_CR74","unstructured":"Terese: Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"key":"28_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60675-0_35","volume-title":"Funtional Programming Languages in Education","author":"DA Turner","year":"1995","unstructured":"Turner, D.A.: Elementary strong functional programming. In: Hartel, P.H., Plasmeijer, R. (eds.) FPLE 1995. LNCS, vol. 1022, pp. 1\u201313. Springer, Heidelberg (1995). \n                      https:\/\/doi.org\/10.1007\/3-540-60675-0_35"},{"issue":"1","key":"28_CR76","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1016\/j.apal.2006.12.001","volume":"146","author":"B Berg van den","year":"2007","unstructured":"van den Berg, B., de Marchi, F.: Non-well-founded trees in categories. Ann. Pure Appl. Logic 146(1), 40\u201359 (2007). \n                      https:\/\/doi.org\/10.1016\/j.apal.2006.12.001","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1\u20133","key":"28_CR77","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1016\/j.tcs.2004.12.009","volume":"338","author":"J Worrell","year":"2005","unstructured":"Worrell, J.: On the final sequence of a finitary set functor. Theor. Comput. Sci. 338(1\u20133), 184\u2013199 (2005). \n                      https:\/\/doi.org\/10.1016\/j.tcs.2004.12.009","journal-title":"Theor. Comput. Sci."}],"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-17184-1_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:23:57Z","timestamp":1558344237000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17184-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171834","9783030171841"],"references-count":77,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17184-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"6 April 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","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":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/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"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"86","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - 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"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}