{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T02:47:40Z","timestamp":1764557260085},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642253171"},{"type":"electronic","value":"9783642253188"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-25318-8_26","type":"book-chapter","created":{"date-parts":[[2011,12,3]],"date-time":"2011-12-03T21:54:45Z","timestamp":1322949285000},"page":"353-368","source":"Crossref","is-referenced-by-count":9,"title":["A Proof Pearl with the Fan Theorem and Bar Induction"],"prefix":"10.1007","author":[{"given":"Keiko","family":"Nakata","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tarmo","family":"Uustalu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Bezem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"26_CR1","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1002\/malq.200410038","volume":"51","author":"J. Berger","year":"2005","unstructured":"Berger, J., Ishihara, H.: Brouwer\u2019s fan theorem and unique existence in constructive analysis. Math. Log. Quart.\u00a051(4), 360\u2013364 (2005)","journal-title":"Math. Log. Quart."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Berger, U.: From coinductive proofs to exact real arithmetic: theory and applications. Logical Methods in Comput. Sci.\u00a07(1) (2011)","DOI":"10.2168\/LMCS-7(1:8)2011"},{"key":"26_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Bezem, M., Nakata, K., Uustalu, T.: On streams that are finitely red (submitted for publication 2011) (manuscript)","DOI":"10.2168\/LMCS-8(4:4)2012"},{"key":"26_CR5","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)"},{"key":"26_CR6","unstructured":"Coquand, T., Spiwack, A.: Constructively finite? In: Laureano Lamb\u00e1n, L., Romero, A., Rubio, J. (eds.) Scientific Contributions in Honor of Mirian Andr\u00e9s G\u00f3mez Universidad de La Rioja (2010)"},{"issue":"6","key":"26_CR7","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1093\/logcom\/13.6.801","volume":"13","author":"S. Coupet-Grimal","year":"2003","unstructured":"Coupet-Grimal, S.: An axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions. J. of Logic and Comput.\u00a013(6), 801\u2013813 (2003)","journal-title":"J. of Logic and Comput."},{"issue":"1","key":"26_CR8","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theor. Comput. Sci.\u00a0126(1), 77\u201396 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-13321-3_8","volume-title":"Mathematics of Program Construction","author":"N.A. Danielsson","year":"2010","unstructured":"Danielsson, N.A., Altenkirch, T.: Subtyping, declaratively: an exercise in mixed induction and coinduction. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol.\u00a06120, pp. 100\u2013118. Springer, Heidelberg (2010)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 905\u20131072. MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"issue":"2","key":"26_CR11","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1017\/S0960129509990351","volume":"20","author":"M.H. Escard\u00f3","year":"2010","unstructured":"Escard\u00f3, M.H., Oliva, P.: Selection functions, bar recursion and backward induction. Math. Struct. in Comput. Sci.\u00a020(2), 127\u2013168 (2010)","journal-title":"Math. Struct. in Comput. Sci."},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Escard\u00f3, M.H., Oliva, P.: What sequential games, the Tychonoff Theorem and the double-negation shift have in common. In: Proc. of 3rd ACM SIGPLAN Wksh. on Mathematically Structured Functional Programming, MSFP 2010, pp. 21\u201332. ACM Press (2010)","DOI":"10.1145\/1863597.1863605"},{"issue":"3","key":"26_CR13","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1002\/malq.19900360307","volume":"36","author":"H. Ishihara","year":"1990","unstructured":"Ishihara, H.: An omniscience principle, the K\u00f6nig Lemma and the Hahn-Banach theorem. Math. Log. Quart.\u00a036(3), 237\u2013240 (1990)","journal-title":"Math. Log. Quart."},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1305\/ndjfl\/1153858649","volume":"47","author":"H. Ishihara","year":"2006","unstructured":"Ishihara, H.: Weak K\u00f6nig\u2019s lemma implies Brouwer\u2019s fan theorem: a direct proof. Notre Dame J. of Formal Logic\u00a047(2), 249\u2013252 (2006)","journal-title":"Notre Dame J. of Formal Logic"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Hancock, P., Pattinson, D., Ghani, N.: Representations of stream processors using nested fixed points. Logical Methods in Comput. Sci.\u00a05(3) (2009)","DOI":"10.2168\/LMCS-5(3:9)2009"},{"issue":"1-2","key":"26_CR16","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0168-0072(91)90069-X","volume":"51","author":"N.P. Mendler","year":"1991","unstructured":"Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Ann. of Pure and Appl. Logic\u00a051(1-2), 159\u2013172 (1991)","journal-title":"Ann. of Pure and Appl. Logic"},{"issue":"1","key":"26_CR17","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1006\/inco.2000.2902","volume":"164","author":"M. Miculan","year":"2001","unstructured":"Miculan, M.: On the formalization of the modal \u03bc-Calculus in the Calculus of Inductive Constructions. Inform. and Comput.\u00a0164(1), 199\u2013231 (2001)","journal-title":"Inform. and Comput."},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Nakata, K., Uustalu, T.: Resumptions, weak bisimilarity and big-step semantics for While with interactive I\/O: an exercise in mixed induction-coinduction. In: Aceto, L., Sobocinski, P. (eds.) Proc. of 7th Wksh. on Structural Operational Semantics, SOS 2010, Electron. Proc. in Theor. Comput. Sci., vol.\u00a032, pp. 57\u201375 (2010)","DOI":"10.4204\/EPTCS.32.5"},{"key":"26_CR19","unstructured":"Raffalli, C.: L\u2019 Arithm\u00e9tiques Fonctionnelle du Second Ordre avec Points Fixes. PhD thesis, Universit\u00e9 Paris VII (1994)"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0054171","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Sprenger","year":"1998","unstructured":"Sprenger, C.: A Verified Model Checker for the Modal \u03bc-calculus in Coq. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 167\u2013183. Springer, Heidelberg (1998)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-77505-8_25","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"M.-H. Tsai","year":"2008","unstructured":"Tsai, M.-H., Wang, B.-Y.: Formalization of CTL* in Calculus of Inductive Constructions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 316\u2013330. Springer, Heidelberg (2008)"},{"key":"26_CR22","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics, vol.\u00a0I, II. North-Holland (1988)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25318-8_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,20]],"date-time":"2019-06-20T08:00:35Z","timestamp":1561017635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25318-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253171","9783642253188"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25318-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}