{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T14:24:51Z","timestamp":1791296691242,"version":"4.1.0"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2014,11,17]],"date-time":"2014-11-17T00:00:00Z","timestamp":1416182400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,10]]},"abstract":"<jats:p>This paper deals with the specification problem in classical realizability (such as introduced by Krivine (2009 <jats:italic>Panoramas et synth\u00e9ses<\/jats:italic><jats:bold>27<\/jats:bold>)), which is to characterize the universal realizers of a given formula by their computational behaviour. After recalling the framework of classical realizability, we present the problem in the general case and illustrate it with some examples. In the rest of the paper, we focus on Peirce's law, and present two game-theoretic characterizations of its universal realizers. First, we consider the particular case where the language of realizers contains no extra instruction such as \u2018quote\u2019 (Krivine 2003 <jats:italic>Theoretical Computer Science<\/jats:italic><jats:bold>308<\/jats:bold> 259\u2013276). We present a first game <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000450_inline1\"\/><jats:tex-math>$\\mathds{G}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sub>0<\/jats:sub> and show that the universal realizers of Peirce's law can be characterized as the uniform winning strategies for <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000450_inline1\"\/><jats:tex-math>$\\mathds{G}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sub>0<\/jats:sub>, using the technique of interaction constants. Then we show that in the presence of extra instructions such as \u2018quote\u2019, winning strategies for the game <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000450_inline1\"\/><jats:tex-math>$\\mathds{G}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sub>0<\/jats:sub> are still adequate but no more complete. For that, we exhibit an example of a wild realizer of Peirce's law, that introduces a purely game-theoretic form of backtrack that is not captured by <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000450_inline1\"\/><jats:tex-math>$\\mathds{G}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sub>0<\/jats:sub>. We finally propose a more sophisticated game <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000450_inline1\"\/><jats:tex-math>$\\mathds{G}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sub>1<\/jats:sub>, and show that winning strategies for the game <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0960129514000450_inline1\"\/><jats:tex-math>$\\mathds{G}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula><jats:sub>1<\/jats:sub> are both adequate and complete in the general case, without any further assumption about the instruction set used by the language of classical realizers.<\/jats:p>","DOI":"10.1017\/s0960129514000450","type":"journal-article","created":{"date-parts":[[2014,11,17]],"date-time":"2014-11-17T14:02:16Z","timestamp":1416232936000},"page":"1269-1303","source":"Crossref","is-referenced-by-count":4,"title":["Specifying Peirce's law in classical realizability"],"prefix":"10.1017","volume":"26","author":[{"given":"MAURICIO","family":"GUILLERMO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ALEXANDRE","family":"MIQUEL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,11,17]]},"reference":[{"key":"S0960129514000450_ref20","unstructured":"McCarty D. (1984) Realizability and Recursive Mathematics, Ph.D. thesis, Carnegie-Mellon University."},{"key":"S0960129514000450_ref19","first-page":"127","article-title":"An intuitionistic theory of types. In twenty-five years of constructive type theory.","volume":"36","author":"Martin-L\u00f6f","year":"1998","journal-title":"Oxford Logic Guides"},{"key":"S0960129514000450_ref3","volume-title":"The Calculi of Lambda-Conversion","author":"Church","year":"1941"},{"key":"S0960129514000450_ref26","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990074"},{"key":"S0960129514000450_ref25","doi-asserted-by":"publisher","DOI":"10.2307\/2275652"},{"key":"S0960129514000450_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00776-4"},{"key":"S0960129514000450_ref11","doi-asserted-by":"crossref","unstructured":"Griffin T. (1990) A formulae-as-types notion of control. In: Principles of Programming Languages 47\u201358.","DOI":"10.1145\/96709.96714"},{"key":"S0960129514000450_ref24","first-page":"207","article-title":"On Krivine's realizability interpretation of classical second-order arithmetic.","volume":"84","author":"Oliva","year":"2008","journal-title":"Fundamenta Informaticae"},{"key":"S0960129514000450_ref13","unstructured":"Howard W. A. (1969) The formulae-as-types notion of construction. Privately circulated notes."},{"key":"S0960129514000450_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066775"},{"key":"S0960129514000450_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s001530000057"},{"key":"S0960129514000450_ref10","doi-asserted-by":"publisher","DOI":"10.2307\/2274230"},{"key":"S0960129514000450_ref5","volume-title":"Combinatory Logic","author":"Curry","year":"1958"},{"key":"S0960129514000450_ref2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0025"},{"key":"S0960129514000450_ref1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S0960129514000450_ref15","volume-title":"Lambda-Calculus, Types and Models","author":"Krivine","year":"1993"},{"key":"S0960129514000450_ref9","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129514000450_ref12","unstructured":"Guillermo M. (2008) Jeux de r\u00e9alisabilit\u00e9 en arithm\u00e9tique classique, Ph.D. thesis, Universit\u00e9 Paris 7."},{"key":"S0960129514000450_ref18","first-page":"197","article-title":"Realizability in classical logic. In: interactive models of computation and program behaviour.","volume":"27","author":"Krivine","year":"2009","journal-title":"Panoramas et synth\u00e8ses"},{"key":"S0960129514000450_ref4","doi-asserted-by":"crossref","unstructured":"Curien P.-L. and Herbelin H. (2000) The duality of computation. In: International Conference on Functional Programming 233\u2013243.","DOI":"10.1145\/351240.351262"},{"key":"S0960129514000450_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_25"},{"key":"S0960129514000450_ref14","doi-asserted-by":"publisher","DOI":"10.2307\/2269016"},{"key":"S0960129514000450_ref22","first-page":"1","article-title":"Existential witness extraction in classical realizability and via a negative translation","volume":"7","author":"Miquel","year":"2010","journal-title":"Logical Methods for Computer Science"},{"key":"S0960129514000450_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066773"},{"key":"S0960129514000450_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0103100"},{"key":"S0960129514000450_ref8","volume-title":"Le point aveugle \u2013 Cours de logique \u2013 Volume I \u2013 vers la perfection","author":"Girard","year":"2006"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000450","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T22:01:34Z","timestamp":1555624894000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000450\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,17]]},"references-count":26,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["S0960129514000450"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000450","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,17]]}}}