{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:25Z","timestamp":1759638805831,"version":"3.37.3"},"reference-count":31,"publisher":"Oxford University Press (OUP)","issue":"4","license":[{"start":{"date-parts":[[2017,1,17]],"date-time":"2017-01-17T00:00:00Z","timestamp":1484611200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"funder":[{"name":"LabEx CARMIN"},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P25781"],"award-info":[{"award-number":["P25781"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,6,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>During the last 20 years or so, a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work, we present the many variants of bar recursion used in this context as instantiations of a parametrized form of backward recursion, and give a uniform proof that under certain conditions this recursor realizes a corresponding family of parametrized dependent choice principles. From this proof, the soundness of most of the existing bar recursive realizability interpretations of choice, including those based on the Berardi\u2013Bezem\u2013Coquand functional, modified realizability and the more recent products of selection functions of Escard\u00f3 and Oliva, follows as a simple corollary. We achieve not only a uniform framework in which familiar realizability interpretations of choice can be compared, but show that these represent just simple instances of a large family of potential interpretations of dependent choice principles.<\/jats:p>","DOI":"10.1093\/logcom\/exv056","type":"journal-article","created":{"date-parts":[[2017,2,13]],"date-time":"2017-02-13T16:00:04Z","timestamp":1487001604000},"page":"519-554","source":"Crossref","is-referenced-by-count":1,"title":["Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice"],"prefix":"10.1093","volume":"29","author":[{"given":"Thomas","family":"Powell","sequence":"first","affiliation":[{"name":"Institute of Computer Science, University of Innsbruck"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2019,7,8]]},"reference":[{"key":"2019070814353658000_B1"},{"key":"2019070814353658000_B2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1002\/1521-3870(200201)48:1<3::AID-MALQ3>3.0.CO;2-6","article-title":"Update procedures and the 1-consistency of arithmetic","volume":"48","author":"Avigad","year":"2002","journal-title":"Mathematical Logic Quarterly"},{"key":"2019070814353658000_B3","doi-asserted-by":"crossref","first-page":"600","DOI":"10.2307\/2586854","article-title":"On the computational content of the axiom of choice","volume":"63","author":"Berardi","year":"1998","journal-title":"Journal of Symbolic Logic"},{"key":"2019070814353658000_B4"},{"key":"2019070814353658000_B5"},{"key":"2019070814353658000_B6","first-page":"89","article-title":"Modified bar recursion and classical dependent choice","volume":"20","author":"Berger","year":"2005","journal-title":"Lecture Notes in Logic"},{"key":"2019070814353658000_B7","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1017\/S0960129506005093","article-title":"Modified bar recursion","volume":"16","author":"Berger","year":"2006","journal-title":"Mathematical Structures in Computer Science"},{"key":"2019070814353658000_B8"},{"key":"2019070814353658000_B9","doi-asserted-by":"crossref","first-page":"652","DOI":"10.2307\/2274319","article-title":"Strongly majorizable functionals of finite type: A model for bar recursion containing discontinuous functionals","volume":"50","author":"Bezem","year":"1985","journal-title":"Journal of Symbolic Logic"},{"key":"2019070814353658000_B10"},{"key":"2019070814353658000_B11","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1006\/inco.1994.1034","article-title":"An analysis of Ramsey's theorem","volume":"110","author":"Coquand","year":"1994","journal-title":"Information and Computation"},{"key":"2019070814353658000_B12"},{"key":"2019070814353658000_B13","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1017\/S0960129509990351","article-title":"Selection functions, bar recursion and backward induction","volume":"20","author":"Escard\u00f3","year":"2010","journal-title":"Mathematical Structures in Computer Science"},{"key":"2019070814353658000_B14","doi-asserted-by":"crossref","first-page":"1519","DOI":"10.1098\/rspa.2010.0471","article-title":"Sequential games and optimal strategies","volume":"467","author":"Escard\u00f3","year":"2011","journal-title":"Royal Society Proceedings A"},{"key":"2019070814353658000_B15","doi-asserted-by":"crossref","first-page":"681","DOI":"10.1016\/j.apal.2011.11.002","article-title":"The Peirce translation","volume":"163","author":"Escard\u00f3","year":"2012","journal-title":"Annals of Pure and Applied Logic"},{"key":"2019070814353658000_B16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/jsl.2014.82","article-title":"Bar recursion and products of selection functions","volume":"80","author":"Escard\u00f3","year":"2015","journal-title":"Journal of Symbolic Logic"},{"key":"2019070814353658000_B17","first-page":"81","article-title":"Countable functionals","volume-title":"Constructivity in Mathematics","author":"Kleene","year":"1959"},{"key":"2019070814353658000_B18"},{"key":"2019070814353658000_B19","first-page":"101","article-title":"Interpretation of analysis by means of functionals of finite type","volume-title":"Constructivity in Mathematics","author":"Kreisel","year":"1959"},{"key":"2019070814353658000_B20","doi-asserted-by":"crossref","first-page":"833","DOI":"10.1017\/S0305004100003844","article-title":"On well-quasi-ordering finite trees","volume":"59","author":"Nash-Williams","year":"1963","journal-title":"Proceedings of the Cambridge Philosophical Society"},{"key":"2019070814353658000_B21","first-page":"230","article-title":"On the consistency of certain logical calculi","volume":"12","author":"Novikoff","year":"1943","journal-title":"Matematiceskij Sbornik"},{"key":"2019070814353658000_B22","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1002\/malq.201100106","article-title":"On Spector's bar recursion","volume":"58","author":"Oliva","year":"2012","journal-title":"Mathematical Logic Quarterly"},{"key":"2019070814353658000_B23"},{"key":"2019070814353658000_B24"},{"key":"2019070814353658000_B25","doi-asserted-by":"crossref","first-page":"1727","DOI":"10.1016\/j.apal.2014.07.003","article-title":"The equivalence of bar recursion and open recursion","volume":"165","author":"Powell","year":"2014","journal-title":"Annals of Pure and Applied Logic"},{"key":"2019070814353658000_B26","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/0020-0190(88)90126-3","article-title":"Proving open properties by induction","volume":"29","author":"Raoult","year":"1988","journal-title":"Information Processing Letters"},{"key":"2019070814353658000_B27"},{"key":"2019070814353658000_B28","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/j.apal.2008.01.004","article-title":"Programs from proofs using classical dependent choice","volume":"153","author":"Seisenberger","year":"2008","journal-title":"Annals of Pure and Applied Logic"},{"key":"2019070814353658000_B29"},{"key":"2019070814353658000_B30"},{"key":"2019070814353658000_B31"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/29\/4\/519\/28917490\/exv056.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T20:42:33Z","timestamp":1569184953000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/29\/4\/519\/2917831"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,6]]},"references-count":31,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2019,7,8]]},"published-print":{"date-parts":[[2019,6,6]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exv056","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2019,8,1]]},"published":{"date-parts":[[2019,6,6]]}}}