{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:19:50Z","timestamp":1725851990885},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496299"},{"type":"electronic","value":"9783662496305"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-662-49630-5_6","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T09:04:32Z","timestamp":1458551072000},"page":"91-106","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Coalgebraic View of Bar Recursion and Bar Induction"],"prefix":"10.1007","author":[{"given":"Venanzio","family":"Capretta","sequence":"first","affiliation":[]},{"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"6_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. Theoret. Comput. Sci. 342(1), 3\u201327 (2005)","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"6_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1051\/ita:2007028","volume":"41","author":"J Ad\u00e1mek","year":"2007","unstructured":"Ad\u00e1mek, J., L\u00fccke, D., Milius, S.: Recursive coalgebras of finitary functors. Theoret. Inform. Appl. 41(4), 447\u2013462 (2007)","journal-title":"Theoret. Inform. Appl."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Ad\u00e1mek, J., Milius, S., Moss, L.S., Sousa, L.: Well-pointed coalgebras. Log. Methods Comput. Sci. 9(3), article 2 (2013)","DOI":"10.2168\/LMCS-9(3:2)2013"},{"key":"6_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139032636","volume-title":"Lambda Calculus with Types: Perspectives in Logic","author":"HP Barendregt","year":"2013","unstructured":"Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types: Perspectives in Logic. Cambridge University Press, Cambridge (2013)"},{"issue":"2","key":"6_CR5","doi-asserted-by":"publisher","first-page":"600","DOI":"10.2307\/2586854","volume":"63","author":"S Berardi","year":"1998","unstructured":"Berardi, S., Bezem, M., Coquand, T.: On the computational content of the axiom of choice. J. Symb. Log. 63(2), 600\u2013622 (1998)","journal-title":"J. Symb. Log."},{"issue":"2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1017\/S0960129506005093","volume":"16","author":"U Berger","year":"2006","unstructured":"Berger, U., Oliva, P.: Modified bar recursion. Math. Struct. Comput. Sci. 16(2), 163\u2013183 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"4","key":"6_CR7","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/j.ic.2005.08.005","volume":"204","author":"V Capretta","year":"2006","unstructured":"Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Inf. Comput. 204(4), 437\u2013468 (2006)","journal-title":"Inf. Comput."},{"key":"6_CR8","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)"},{"key":"6_CR9","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198505242.001.0001","volume-title":"Elements of Intuitionism","author":"M Dummett","year":"2000","unstructured":"Dummett, M.: Elements of Intuitionism, 2nd edn. Oxford Science Publications, Oxford (2000)","edition":"2"},{"issue":"2","key":"6_CR10","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1017\/S0960129509990351","volume":"20","author":"MH Escard\u00f3","year":"2010","unstructured":"Escard\u00f3, M.H., Oliva, P.: Selection functions, bar recursion and backward induction. Math. Struct. Comput. Sci. 20(2), 127\u2013168 (2010)","journal-title":"Math. Struct. Comput. Sci."},{"key":"6_CR11","unstructured":"Escard\u00f3, M.H., Xu, C.: The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In: Altenkirch, T. (ed.) 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, Leibniz International Proceedings in Informatics, vol. 38, pp. 153\u2013164. Dagstuhl Publishing, Saarbr\u00fccken (2015)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-24849-1_14","volume-title":"Types for Proofs and Programs","author":"N Gambino","year":"2004","unstructured":"Gambino, N., Hyland, M.: Wellfounded trees and dependent polynomial functors. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 210\u2013225. Springer, Heidelberg (2004)"},{"issue":"1","key":"6_CR13","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/j.entcs.2006.06.009","volume":"164","author":"N Ghani","year":"2006","unstructured":"Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electron. Notes Theoret. Comput. Sci. 164(1), 141\u2013155 (2006)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Hancock, P., Pattinson, D., Ghani, N.: Representations of stream processors using nested fixed points. Log. Methods Comput. Sci. 5(3), article 9 (2009)","DOI":"10.2168\/LMCS-5(3:9)2009"},{"issue":"6","key":"6_CR15","doi-asserted-by":"publisher","first-page":"875","DOI":"10.1017\/S096012950200378X","volume":"12","author":"B Jacobs","year":"2002","unstructured":"Jacobs, B.: The temporal logic of coalgebras via Galois algebras. Math. Struct. Comput. Sci. 12(6), 875\u2013903 (2002)","journal-title":"Math. Struct. Comput. Sci."},{"key":"6_CR16","volume-title":"The Foundations of Intuitionistic Mathematics: Especially in Relation to Recursive Functions","author":"S Kleene","year":"1965","unstructured":"Kleene, S., Vesley, R.: The Foundations of Intuitionistic Mathematics: Especially in Relation to Recursive Functions. North-Holland, Amsterdam (1965)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-25318-8_26","volume-title":"Programming Languages and Systems","author":"K Nakata","year":"2011","unstructured":"Nakata, K., Uustalu, T., Bezem, M.: A proof pearl with the fan theorem and bar induction. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 353\u2013368. Springer, Heidelberg (2011)"},{"issue":"1","key":"6_CR18","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0022-4049(74)90032-2","volume":"4","author":"G Osius","year":"1974","unstructured":"Osius, G.: Categorical set theory: a characterization of the category of sets. J. Pure Appl. Algebra 4(1), 79\u2013119 (1974)","journal-title":"J. Pure Appl. Algebra"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In: Dekker, F.D.E. (ed.) Recursive Function Theory: Proceedings of Symposia in Pure Mathematics. vol. 5, pp. 1\u201327. American Mathematical Society, Providence, RI (1962)","DOI":"10.1090\/pspum\/005\/0154801"},{"issue":"3","key":"6_CR20","doi-asserted-by":"publisher","first-page":"705","DOI":"10.2307\/2275781","volume":"61","author":"P Taylor","year":"1996","unstructured":"Taylor, P.: Intuitionistic sets and ordinals. J. Symb. Logic 61(3), 705\u2013744 (1996)","journal-title":"J. Symb. Logic"},{"key":"6_CR21","unstructured":"Taylor, P.: Towards a unified treatment of induction, I: The general recursion theorem. Manuscript (1996)"},{"key":"6_CR22","series-title":"Cambridge Studies in Advanced Mathematics","volume-title":"Practical Foundations of Mathematics","author":"P Taylor","year":"1999","unstructured":"Taylor, P.: Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge (1999)"},{"key":"6_CR23","volume-title":"Choice Sequences","author":"A Troelstra","year":"1977","unstructured":"Troelstra, A.: Choice Sequences. Clarendon Press, Oxford (1977)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49630-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,15]],"date-time":"2024-06-15T04:49:10Z","timestamp":1718426950000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49630-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496299","9783662496305"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49630-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}