{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:53:29Z","timestamp":1773096809293,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642022722","type":"print"},{"value":"9783642022739","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02273-9_4","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T10:12:17Z","timestamp":1246011137000},"page":"20-34","source":"Crossref","is-referenced-by-count":5,"title":["Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1"],"prefix":"10.1007","author":[{"given":"Federico","family":"Aschieri","sequence":"first","affiliation":[]},{"given":"Stefano","family":"Berardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"4_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1002\/1521-3870(200201)48:1<3::AID-MALQ3>3.0.CO;2-6","volume":"48","author":"J. Avigad","year":"2002","unstructured":"Avigad, J.: Update Procedures and the 1-Consistency of Arithmetic. Math. Log. Q.\u00a048(1), 3\u201313 (2002)","journal-title":"Math. Log. Q."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. In: LICS 2004, pp. 192\u2013201 (2004)","DOI":"10.1109\/LICS.2004.1319613"},{"key":"4_CR3","unstructured":"Aschieri, F., Berardi, S.: An Interactive Realizability... (Full Paper), Tech. Rep., Un. of Turin (2009), \n                  \n                    http:\/\/www.di.unito.it\/~stefano\/Realizers2009.pdf"},{"issue":"1","key":"4_CR4","first-page":"167","volume":"15","author":"S. Berardi","year":"2005","unstructured":"Berardi, S.: Classical Logic as Limit .... MSCS\u00a015(1), 167\u2013200 (2005)","journal-title":"MSCS"},{"issue":"1-3","key":"4_CR5","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.apal.2005.04.006","volume":"139","author":"S. Berardi","year":"2006","unstructured":"Berardi, S.: Some intuitionistic equivalents of classical principles for degree 2 formulas. Annals of Pure and Applied Logic\u00a0139(1-3), 185\u2013200 (2006)","journal-title":"Annals of Pure and Applied Logic"},{"key":"4_CR6","unstructured":"Berardi, S., Coquand, T., Hayashi, S.: Games with 1-Bactracking. In: GALOP 2005 (2005)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-87531-4_17","volume-title":"Computer Science Logic","author":"S. Berardi","year":"2008","unstructured":"Berardi, S., de\u2019Liguoro, U.: A calculus of realizers for EM\n                1-Arithmetic. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 215\u2013229. Springer, Heidelberg (2008)"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"325","DOI":"10.2307\/2275524","volume":"60","author":"T. Coquand","year":"1995","unstructured":"Coquand, T.: A Semantic of Evidence for Classical Arithmetic. Journal of Symbolic Logic\u00a060, 325\u2013337 (1995)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02962-6","volume-title":"Logic and Structure","author":"D.v. Dalen","year":"1994","unstructured":"Dalen, D.v.: Logic and Structure, 3rd edn. Springer-, Heidelberg (1994)","edition":"3"},{"key":"4_CR10","volume-title":"Proofs and Types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y.: Proofs and Types. Cambridge University Press, Cambridge (1989)"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"28","DOI":"10.2307\/2270580","volume":"30","author":"E.M. Gold","year":"1965","unstructured":"Gold, E.M.: Limiting Recursion. Journal of Symbolic Logic\u00a030, 28\u201348 (1965)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Hayashi, S., Sumitomo, R., Shii, K.: Towards Animation of Proofs -Testing Proofs by Examples. Theoretical Computer Science (2002)","DOI":"10.1016\/S0304-3975(00)00350-9"},{"issue":"4","key":"4_CR13","first-page":"331","volume":"77","author":"S. Hayashi","year":"2007","unstructured":"Hayashi, S.: Can Proofs be Animated by Games? FI\u00a077(4), 331\u2013343 (2007)","journal-title":"FI"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.tcs.2005.10.019","volume":"350","author":"S. Hayashi","year":"2006","unstructured":"Hayashi, S.: Mathematics based on incremental learning - Excluded Middle and Inductive Inference. Theoretical Computer Science\u00a0350, 125\u2013139 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"4_CR15","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"S.C. Kleene","year":"1945","unstructured":"Kleene, S.C.: On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic\u00a010(4), 109\u2013124 (1945)","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR16","volume-title":"The Logic of Scientific Discovery","author":"K. Popper","year":"2002","unstructured":"Popper, K.: The Logic of Scientific Discovery. Routledge Classics, Routledge (2002)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02273-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T20:05:06Z","timestamp":1552075506000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02273-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642022722","9783642022739"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02273-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}