{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T16:19:27Z","timestamp":1790439567892,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662544334","type":"print"},{"value":"9783662544341","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/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-662-54434-1_2","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T04:20:06Z","timestamp":1489810806000},"page":"29-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Generalizing Inference Systems by Coaxioms"],"prefix":"10.1007","author":[{"given":"Davide","family":"Ancona","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Francesco","family":"Dagnino","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Elena","family":"Zucca","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Handbook of Mathematical Logic. North Holland (1977)","DOI":"10.1016\/S0049-237X(08)71120-0"},{"issue":"6","key":"2_CR2","doi-asserted-by":"publisher","first-page":"1085","DOI":"10.1017\/S0960129506005706","volume":"16","author":"J Ad\u00e1mek","year":"2006","unstructured":"Ad\u00e1mek, J., Milius, S., Velebil, J.: Iterative algebras at work. Math. Struct. Comput. Sci. 16(6), 1085\u20131131 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Ancona, D.: Regular corecursion in Prolog. In: SAC 2012 - ACM Symposium on Applied Computing, pp. 1897\u20131902 (2012)","DOI":"10.1145\/2245276.2232088"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/978-3-642-31057-7_21","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"D Ancona","year":"2012","unstructured":"Ancona, D.: Soundness of object-oriented languages with coinductive big-step semantics. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 459\u2013483. Springer, Heidelberg (2012)"},{"issue":"4","key":"2_CR5","first-page":"142","volume":"39","author":"D Ancona","year":"2013","unstructured":"Ancona, D.: Regular corecursion in Prolog. Comput. Lang. Syst. Struct. 39(4), 142\u2013162 (2013)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Ancona, D.: How to prove type soundness of Java-like languages without forgoing big-step semantics. In: FTfJP 2014 - Formal Techniques for Java-like Programs, pp. 1:1\u20131:6. ACM Press (2014)","DOI":"10.1145\/2635631.2635846"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-662-44202-9_12","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"D Ancona","year":"2014","unstructured":"Ancona, D., Corradi, A.: Sound and complete subtyping between coinductive types for object-oriented languages. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 282\u2013307. Springer, Heidelberg (2014)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Ancona, D., Dagnino, F., Zucca, E.: Towards a model of corecursion with default. In: FTfJP 2016 - Formal Techniques for Java-like Programs (2016)","DOI":"10.1145\/2955811.2955820"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-03013-0_2","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"D Ancona","year":"2009","unstructured":"Ancona, D., Lagorio, G.: Coinductive type systems for object-oriented languages. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 2\u201326. Springer, Heidelberg (2009)"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Ancona, D., Zucca, E.: Corecursive featherweight Java. In: FTfJP 2012 - Formal Techniques for Java-like Programs (2012)","DOI":"10.1145\/2318202.2318205"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Ancona, D., Zucca, E.: Safe corecursion in coFJ. In: FTfJP 2013 - Formal Techniques for Java-like Programs (2012)","DOI":"10.1145\/2489804.2489807"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-10452-7_7","volume-title":"Formal Methods: Foundations and Applications","author":"V Capretta","year":"2009","unstructured":"Capretta, V., Uustalu, T., Vene, V.: Corecursive algebras: a study of general structured corecursion. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 84\u2013100. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-10452-7_7"},{"key":"2_CR13","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)"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretations. In: ACM Symposium on Principles of Programming Languages, pp. 83\u201394. ACM Press (1992)","DOI":"10.1145\/143165.143184"},{"key":"2_CR15","unstructured":"Grall, H.: Proving fixed point. In: FICS 2010 - Fixed Points in Computer Science (2010)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Hughes, J., Moran, A.: Making choices lazily. In: FPCA 1995 - Functional Programming Languages and Computer Architecture, pp. 108\u2013119. ACM Press (1995)","DOI":"10.1145\/224164.224191"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Hur, C., Neis, G., Dreyer, D., Vafeiadis, V.: The power of parameterization in coinductive proof. In: ACM Symposium on Principles of Programming Languages, pp. 193\u2013206 (2013)","DOI":"10.1145\/2480359.2429093"},{"key":"2_CR18","unstructured":"Jeannin, J., Kozen, D., Silva, A.: CoCaml: programming with coinductive types. Technical report, Computing and Information Science, Cornell University, December 2012"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-37036-6_4","volume-title":"Programming Languages and Systems","author":"J-B Jeannin","year":"2013","unstructured":"Jeannin, J.-B., Kozen, D., Silva, A.: Language constructs for non-well-founded computation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 61\u201380. Springer, Heidelberg (2013)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Jeannin, J., Kozen, D., Silva, A.: Well-founded coalgebras, revisited. Math. Struct. Comput. Sci. FirstView, 1\u201321 (2016)","DOI":"10.1017\/S0960129515000481"},{"key":"2_CR21","unstructured":"Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Technical Communications of (ICLP 2015) (2015)"},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1016\/0020-0190(82)90065-5","volume":"14","author":"J Lassez","year":"1982","unstructured":"Lassez, J., Nguyen, V.L., Sonenberg, L.: Fixed point theorems and semantics: a folk tale. Inf. Process. Lett. 14(3), 112\u2013116 (1982)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"2_CR23","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284\u2013304 (2009)","journal-title":"Inf. Comput."},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Leroy, X., Rouaix, F.: Security properties of typed applets. In: MacQueen, D.B., Cardelli, L. (eds.) ACM Symposium on Principles of Programming Languages, pp. 391\u2013403. ACM Press (1998)","DOI":"10.1145\/268946.268979"},{"issue":"4\u20135","key":"2_CR25","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1017\/S147106841400012X","volume":"14","author":"T Mantadelis","year":"2014","unstructured":"Mantadelis, T., Rocha, R., Moura, P.: Tabling, rational terms, and coinduction finally together!. Theory Pract. Log. Program. 14(4\u20135), 429\u2013443 (2014)","journal-title":"Theory Pract. Log. Program."},{"issue":"1","key":"2_CR26","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0304-3975(91)90033-X","volume":"87","author":"R Milner","year":"1991","unstructured":"Milner, R., Tofte, M.: Co-induction in relational semantics. Theor. Comput. Sci. 87(1), 209\u2013220 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-03359-9_26","volume-title":"Theorem Proving in Higher Order Logics","author":"K Nakata","year":"2009","unstructured":"Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for while. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 375\u2013390. Springer, Heidelberg (2009)"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S1571-0661(04)00056-8","volume":"11","author":"D Pavlovic","year":"1998","unstructured":"Pavlovic, D.: Guarded induction on final coalgebras. Electron. Notes Theor. Comput. Sci. 11, 140\u2013157 (1998)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"2_CR29","unstructured":"Poulsen, C.B., Mosses, P.D.: Flag-based big-step semantics. J. Log. Algebr. Methods Program. (2016). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S2352220816300311"},{"issue":"3","key":"2_CR30","first-page":"237","volume":"10","author":"DA Schmidt","year":"1998","unstructured":"Schmidt, D.A.: Trace-based abstract interpretation of operational semantics. Lisp Symb. Comput. 10(3), 237\u2013271 (1998)","journal-title":"Lisp Symb. Comput."},{"key":"2_CR31","unstructured":"Simon, L.: Extending logic programming with coinduction. Ph.D. thesis, University of Texas at Dallas (2006)"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Simon, L., Bansal, A., Mallya, A., Gupta, G.: Co-logic programming: extending logic programming with coinduction. In: ICALP 2007 - International Colloquium on Automata, Languages and Programming, pp. 472\u2013483 (2007)","DOI":"10.1007\/978-3-540-73420-8_42"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/11799573_25","volume-title":"Logic Programming","author":"L Simon","year":"2006","unstructured":"Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive logic programming. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 330\u2013345. Springer, Heidelberg (2006)"},{"issue":"2","key":"2_CR34","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285\u2013309 (1955)","journal-title":"Pac. J. Math."}],"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-3-662-54434-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T15:41:43Z","timestamp":1635262903000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","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":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","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":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}