{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:28:25Z","timestamp":1750307305037,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2012,4,1]],"date-time":"2012-04-01T00:00:00Z","timestamp":1333238400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,4]]},"abstract":"<jats:p>\n            We propose a realizability interpretation of a system for quantier free arithmetic which is equivalent to the fragment of classical arithmetic without\n            <jats:italic>nested<\/jats:italic>\n            quantifiers, called here\n            <jats:bold>EM<\/jats:bold>\n            <jats:sub>1<\/jats:sub>\n            -arithmetic. We interpret classical proofs as interactive learning strategies, namely as processes going through several stages of knowledge and learning by interacting with the \u201cnature,\u201d represented by the standard interpretation of closed atomic formulas, and with each other. We obtain in this way a program extraction method by proof interpretation, which is faithful with respect to proofs, in the sense that it is compositional and that it does not need any translation.\n          <\/jats:p>","DOI":"10.1145\/2159531.2159533","type":"journal-article","created":{"date-parts":[[2012,4,24]],"date-time":"2012-04-24T18:41:10Z","timestamp":1335292870000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Interactive Realizers"],"prefix":"10.1145","volume":"13","author":[{"given":"Stefano","family":"Berardi","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Torino"}]},{"given":"Ugo","family":"de\u2019Liguoro","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Torino"}]}],"member":"320","published-online":{"date-parts":[[2012,4]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.5555\/1018438.1021855"},{"volume-title":"Proceedings of Classical Logic and Computation","year":"2010","author":"Aschieri F.","key":"e_1_2_1_2_1"},{"unstructured":"Aschieri F. 2011. Learning realizability games and classical logic. Ph.D. Thesis Queen Mary University of London. Aschieri F. 2011. Learning realizability games and classical logic. Ph.D. Thesis Queen Mary University of London.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","first-page":"3","article-title":"Interactive learning-based realizability for Heyting arithmetic with EM1","volume":"6","author":"Aschieri F.","year":"2010","journal-title":"Logic. Meth. Comput. Sci."},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1017\/S0960129504004529"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1007\/978-3-540-87531-4_17"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1016\/j.ic.2008.10.003"},{"volume-title":"Proceedings of the Workshop on Games for Logic and Programming Languages. D. R. Ghica and G. McCusker Eds., 210--225","author":"Berardi S.","key":"e_1_2_1_8_1"},{"unstructured":"Caff S. 2010. Costruzione di realizzatori interattivi da prove in PRA+EM1 ed estrazione da Isabelle\/HOL. Masters thesis. Caff S. 2010. Costruzione di realizzatori interattivi da prove in PRA+EM1 ed estrazione da Isabelle\/HOL. Masters thesis.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.2307\/2275524"},{"doi-asserted-by":"crossref","unstructured":"Crole R. L. 1993. Categories for Types. Cambridge University Press. Crole R. L. 1993. Categories for Types . Cambridge University Press.","key":"e_1_2_1_11_1","DOI":"10.1017\/CBO9781139172707"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.2307\/2270580"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1016\/S0019-9958(67)91165-5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1016\/j.tcs.2005.10.019"},{"doi-asserted-by":"crossref","unstructured":"Hilbert D. and Bernays P. 1970. Grundlagen der Mathematik Vol. II. Springer. Hilbert D. and Bernays P. 1970. Grundlagen der Mathematik Vol. II. Springer.","key":"e_1_2_1_15_1","DOI":"10.1007\/978-3-642-86896-2"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1016\/0890-5401(91)90052-4"},{"unstructured":"Rispoli D. 2009. An implementation of interactive realizers for classical arithmetic without nested quantiers. Masters thesis. Rispoli D. 2009. An implementation of interactive realizers for classical arithmetic without nested quantiers. Masters thesis.","key":"e_1_2_1_17_1"},{"unstructured":"Troelstra A. S. and van Dalen D. 1988. Constructivism in Mathematics Vol. 1 2. North-Holland. Troelstra A. S. and van Dalen D. 1988. Constructivism in Mathematics Vol. 1 2. North-Holland.","key":"e_1_2_1_18_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2159531.2159533","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2159531.2159533","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:58Z","timestamp":1750244398000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2159531.2159533"}},"subtitle":["A New Approach to Program Extraction from Nonconstructive Proofs"],"short-title":[],"issued":{"date-parts":[[2012,4]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["10.1145\/2159531.2159533"],"URL":"https:\/\/doi.org\/10.1145\/2159531.2159533","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2012,4]]},"assertion":[{"value":"2010-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}