{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:49:07Z","timestamp":1764557347673,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296036"},{"type":"electronic","value":"9783319296043"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29604-3_9","type":"book-chapter","created":{"date-parts":[[2016,2,20]],"date-time":"2016-02-20T07:53:12Z","timestamp":1455954792000},"page":"126-143","source":"Crossref","is-referenced-by-count":11,"title":["Proof Relevant Corecursive Resolution"],"prefix":"10.1007","author":[{"given":"Peng","family":"Fu","sequence":"first","affiliation":[]},{"given":"Ekaterina","family":"Komendantskaya","sequence":"additional","affiliation":[]},{"given":"Tom","family":"Schrijvers","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Pond","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,21]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1051\/ita\/2011009","volume":"45","author":"D Ancona","year":"2011","unstructured":"Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theor. Inf. Appl. 45(1), 3\u201333 (2011)","journal-title":"RAIRO - Theor. Inf. Appl."},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0054285","volume-title":"Mathematics of Program Construction","author":"RS Bird","year":"1998","unstructured":"Bird, R.S., Meertens, L.: Nested datatypes. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 52\u201367. Springer, Heidelberg (1998)"},{"key":"9_CR3","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.) Gurevich Festschrift II 2015. LNCS, vol. 9300, pp. 24\u201351. Springer, Heidelberg (2015)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (1994)"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N Dershowitz","year":"1987","unstructured":"Dershowitz, N.: Termination of rewriting. J. Symb. Comput. 3, 69\u2013115 (1987)","journal-title":"J. Symb. Comput."},{"key":"9_CR6","unstructured":"Fu, P., Komendantskaya, E.: A type-theoretic approach to resolution. In: 25th International Symposium, LOPSTR 2015. Revised Selected Papers (2015)"},{"issue":"4","key":"9_CR7","first-page":"353","volume":"66","author":"J Gibbons","year":"2005","unstructured":"Gibbons, J., Hutton, G.: Proof methods for corecursive programs. Fundam. Inf. Spec. Issue Program Transform. 66(4), 353\u2013366 (2005)","journal-title":"Fundam. Inf. Spec. Issue Program Transform."},{"key":"9_CR8","unstructured":"Gimenez, C.E.: Un calcul de constructions infinies et son application a la v\u00e9rification de syst\u00e8mes communicants (1996)"},{"key":"9_CR9","volume-title":"Proofs and Types","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types, vol. 7. Cambridge University Press, Cambridge (1989)"},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S1571-0661(05)80542-0","volume":"41","author":"R Hinze","year":"2001","unstructured":"Hinze, R., Peyton-Jones, S.: Derivable type classes. Electron. Notes Theor. Comput. Sci. 41(1), 5\u201335 (2001)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9_CR11","unstructured":"Hughes, J.: Restricted data types in Haskell. In: Haskell Workshop, vol. 99 (1999)"},{"key":"9_CR12","unstructured":"Johann, P., Ghani, N.: Haskell programming with nested types: a principled approach (2009)"},{"key":"9_CR13","unstructured":"Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications of ICLP 2015, July 2015"},{"key":"9_CR14","volume-title":"Qualified Types: Theory and Practice","author":"MP Jones","year":"2003","unstructured":"Jones, M.P.: Qualified Types: Theory and Practice, vol. 9. Cambridge University Press, Cambridge (2003)"},{"key":"9_CR15","unstructured":"Jones, S.P., Jones, M., Meijer, E.: Type classes: an exploration of the design space. In: Haskell Workshopp (1997)"},{"key":"9_CR16","unstructured":"Komendantskaya, E., Johann, P. Structural resolution: a framework for coinductive proof search and proof construction in Horn clause logic. Submitted"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"L\u00e4mmel, R., Peyton-Jones, S.: Scrap your boilerplate with class: extensible generic functions. In: Proceedings of 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, pp. 204\u2013215, New York, NY, USA. ACM (2005)","DOI":"10.1145\/1090189.1086391"},{"key":"9_CR18","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. Springer Science & Business Media, Heidelberg (1987)"},{"issue":"1","key":"9_CR19","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. Log. 51(1), 125\u2013157 (1991)","journal-title":"Ann. Pure Appl. Log."},{"issue":"2","key":"9_CR20","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1093\/jigpal\/5.2.231","volume":"5","author":"LS Moss","year":"1997","unstructured":"Moss, L.S., Danner, N.: On the foundations of corecursion. Log. J. IGPL 5(2), 231\u2013257 (1997)","journal-title":"Log. J. IGPL"},{"key":"9_CR21","first-page":"153","volume":"5","author":"GD Plotkin","year":"1970","unstructured":"Plotkin, G.D.: A note on inductive generalization. Mach. Intell. 5, 153\u2013163 (1970)","journal-title":"Mach. Intell."},{"key":"9_CR22","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., Gupta, G., Mallya, A., Bansal, A.: 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)"},{"issue":"1","key":"9_CR23","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1017\/S0956796806006137","volume":"17","author":"M Sulzmann","year":"2007","unstructured":"Sulzmann, M., Duck, G.J., Peyton Jones, S.L., Stuckey, P.J.: Understanding functional dependencies via constraint handling rules. J. Funct. Program. 17(1), 83\u2013129 (2007)","journal-title":"J. Funct. Program."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 60\u201376. ACM (1989)","DOI":"10.1145\/75277.75283"},{"key":"9_CR25","unstructured":"Zantema, H., Geser, A.: Non-looping rewriting. Universiteit Utrecht, Faculty of Mathematics & Computer Science (1996)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29604-3_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T11:17:45Z","timestamp":1559387865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29604-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296036","9783319296043"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29604-3_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}