{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:14:59Z","timestamp":1725988499492},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999562"},{"type":"electronic","value":"9783319999579"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-99957-9_5","type":"book-chapter","created":{"date-parts":[[2018,8,21]],"date-time":"2018-08-21T08:26:31Z","timestamp":1534839991000},"page":"70-86","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Into the Infinite - Theory Exploration for Coinduction"],"prefix":"10.1007","author":[{"given":"S\u00f3lr\u00fan Halla","family":"Einarsd\u00f3ttir","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moa","family":"Johansson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johannes","family":"\u00c5man\u00a0Pohjola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,22]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"e2","DOI":"10.1017\/S0956796816000022","volume":"26","author":"A Abel","year":"2016","unstructured":"Abel, A., Pientka, B.: Well-founded recursion with copatterns and sized types. J. Funct. Program. 26, e2 (2016)","journal-title":"J. Funct. Program."},{"key":"5_CR2","volume-title":"Introduction to Functional Programming","author":"R Bird","year":"1998","unstructured":"Bird, R.: Introduction to Functional Programming, 2nd edn. Pearson Education, London (1998)","edition":"2"},{"key":"5_CR3","volume-title":"An Introduction to Functional Programming","author":"R Bird","year":"1988","unstructured":"Bird, R., Wadler, P.: An Introduction to Functional Programming. Prentice Hall International (UK) Ltd., Hertfordshire (1988)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-662-54434-1_5","volume-title":"Programming Languages and Systems","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Bouzy, A., Lochbihler, A., Popescu, A., Traytel, D.: Friends with benefits. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 111\u2013140. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_5"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-319-08970-6_7","volume-title":"Interactive Theorem Proving","author":"JC Blanchette","year":"2014","unstructured":"Blanchette, J.C., H\u00f6lzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (Co)datatypes for Isabelle\/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93\u2013110. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_7"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: 2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), pp. 1\u201312, June 2017","DOI":"10.1109\/LICS.2017.8005071"},{"issue":"2","key":"5_CR7","first-page":"9","volume":"38","author":"B Buchberger","year":"2000","unstructured":"Buchberger, B.: Theory exploration with Theorema. Analele Universitatii Din Timisoara, ser. Matematica-Informatica 38(2), 9\u201332 (2000)","journal-title":"Analele Universitatii Din Timisoara, ser. Matematica-Informatica"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of ICFP, pp. 268\u2013279 (2000)","DOI":"10.1145\/351240.351266"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"5_CR10","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). https:\/\/doi.org\/10.1007\/978-3-319-29604-3_9"},{"issue":"5\u20136","key":"5_CR11","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1017\/S0956796810000213","volume":"20","author":"R Hinze","year":"2010","unstructured":"Hinze, R.: Concrete stream calculus: an extended study. J. Funct. Program. 20(5\u20136), 463\u2013535 (2010)","journal-title":"J. Funct. Program."},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"2001","DOI":"10.1016\/S0020-0190(00)00220-9","volume":"79","author":"G Hutton","year":"2001","unstructured":"Hutton, G., Gibbons, J.: The generic approximation lemma. Inf. Proces. Lett. 79, 2001 (2001)","journal-title":"Inf. Proces. Lett."},{"key":"5_CR13","first-page":"222","volume":"62","author":"B Jacobs","year":"1997","unstructured":"Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bull. 62, 222\u2013259 (1997)","journal-title":"EATCS Bull."},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-66107-0_1","volume-title":"Interactive Theorem Proving","author":"M Johansson","year":"2017","unstructured":"Johansson, M.: Automated theory exploration for interactive theorem proving. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 1\u201311. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_1"},{"issue":"3","key":"5_CR15","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10817-010-9193-y","volume":"47","author":"M Johansson","year":"2011","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Conjecture synthesis for inductive theories. J. Autom. Reason. 47(3), 251\u2013289 (2011)","journal-title":"J. Autom. Reason."},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-319-08434-3_9","volume-title":"Intelligent Computer Mathematics","author":"M Johansson","year":"2014","unstructured":"Johansson, M., Ros\u00e9n, D., Smallbone, N., Claessen, K.: Hipster: integrating theory exploration in a proof assistant. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 108\u2013122. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08434-3_9"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Leino, R., Moskal, M.: Co-induction simply: automatic co-inductive proofs in a program verifier. Technical report, Microsoft Research, July 2013","DOI":"10.1007\/978-3-319-06410-9_27"},{"key":"5_CR18","unstructured":"Lochbihler, A.: Coinductive. Archive of Formal Proofs, February 2010. http:\/\/isa-afp.org\/entries\/Coinductive.html . Formal proof development"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-642-03741-2_30","volume-title":"Algebra and Coalgebra in Computer Science","author":"D Lucanu","year":"2009","unstructured":"Lucanu, D., Goriac, E.-I., Caltais, G., Ro\u015fu, G.: CIRC: a behavioral verification tool based on circular coinduction. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 433\u2013442. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03741-2_30"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10489-017-0954-8","volume":"47","author":"RL McCasland","year":"2017","unstructured":"McCasland, R.L., Bundy, A., Smith, P.F.: MATHsAiD: automated mathematical theory exploration. Appl. Intell. 47, 585\u2013606 (2017)","journal-title":"Appl. Intell."},{"key":"5_CR21","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)"},{"issue":"2","key":"5_CR22","doi-asserted-by":"publisher","first-page":"1637","DOI":"10.1016\/j.eswa.2011.06.055","volume":"39","author":"O Montano-Rivas","year":"2012","unstructured":"Montano-Rivas, O., McCasland, R., Dixon, L., Bundy, A.: Scheme-based theorem discovery and concept invention. Expert Syst. Appl. 39(2), 1637\u20131646 (2012)","journal-title":"Expert Syst. Appl."},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-11957-6_26","volume-title":"Programming Languages and Systems","author":"K Nakata","year":"2010","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of while. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 488\u2013506. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_26"},{"key":"5_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9 . http:\/\/isabelle.in.tum.de\/dist\/Isabelle2017\/doc\/tutorial.pdf"},{"key":"5_CR25","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Proceedings of IWIL-2010 (2010)"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Pous, D.: Coinduction all the way up. In: Proceedings of LICS, pp. 307\u2013316. ACM, New York (2016)","DOI":"10.1145\/2933575.2934564"},{"key":"5_CR27","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511777110","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":"5_CR28","doi-asserted-by":"publisher","first-page":"e18","DOI":"10.1017\/S0956796817000090","volume":"27","author":"N Smallbone","year":"2017","unstructured":"Smallbone, N., Johansson, M., Claessen, K., Algehed, M.: Quick specifications for the busy programmer. J. Funct. Program. 27, e18 (2017)","journal-title":"J. Funct. Program."},{"issue":"7","key":"5_CR29","first-page":"751","volume":"10","author":"DA Turner","year":"2004","unstructured":"Turner, D.A.: Total functional programming. J. UCS 10(7), 751\u2013768 (2004)","journal-title":"J. UCS"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99957-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T22:08:36Z","timestamp":1661810916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99957-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999562","9783319999579"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99957-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}