{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:06:38Z","timestamp":1762459598910,"version":"3.37.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319893655"},{"type":"electronic","value":"9783319893662"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89366-2_15","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T19:52:34Z","timestamp":1523649154000},"page":"276-292","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Realizability Interpretation and\u00a0Normalization of Typed Call-by-Need $$\\lambda $$-calculus with Control"],"prefix":"10.1007","author":[{"given":"\u00c9tienne","family":"Miquey","sequence":"first","affiliation":[]},{"given":"Hugo","family":"Herbelin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"issue":"3","key":"15_CR1","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1017\/S0956796897002724","volume":"7","author":"Z Ariola","year":"1993","unstructured":"Ariola, Z., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265\u2013301 (1993)","journal-title":"J. Funct. Program."},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-29822-6_6","volume-title":"Functional and Logic Programming","author":"ZM Ariola","year":"2012","unstructured":"Ariola, Z.M., Downen, P., Herbelin, H., Nakata, K., Saurin, A.: Classical call-by-need sequent calculi: the unity of semantic artifacts. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 32\u201346. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29822-6_6"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A symmetric $$\\lambda $$-calculus for classical program extraction. Inf. Comput. 125(2), 103\u2013117 (1996)","journal-title":"Inf. Comput."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-28869-2_7","volume-title":"Programming Languages and Systems","author":"S Chang","year":"2012","unstructured":"Chang, S., Felleisen, M.: The call-by-need lambda calculus, revisited. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 128\u2013147. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_7"},{"issue":"6","key":"15_CR5","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1017\/S0956796899003512","volume":"9","author":"T Crolard","year":"1999","unstructured":"Crolard, T.: A confluent lambda-calculus with a catch\/throw mechanism. J. Funct. Program. 9(6), 625\u2013647 (1999)","journal-title":"J. Funct. Program."},{"issue":"9","key":"15_CR6","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/357766.351262","volume":"35","author":"Pierre-Louis Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: Proceedings of ICFP 2000, SIGPLAN Notices, vol. 35, no. 9, pp. 233\u2013243. ACM (2000)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR7","unstructured":"Dagand, P.-\u00c9., Scherer, G.: Normalization by realizability also evaluates. In: Baelde, D., Alglave, J. (eds.) Proceedings of JFLA 2015, Le Val d\u2019Ajol, France, January 2015"},{"key":"15_CR8","unstructured":"Felleisen, M., Friedman, D.P., Kohlbecker, E.E., Duba, B.F.: Reasoning with continuations. In: Proceedings of LICS 1986, Cambridge, Massachusetts, USA, 16\u201318 June 1986, pp. 131\u2013141. IEEE Computer Society (1986)"},{"key":"15_CR9","unstructured":"Gallier, J.: On girard\u2019s \u201ccandidats de reductibilit\u00e9\u201d. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 123\u2013203. Academic Press (1900)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Garcia, R., Lumsdaine, A., Sabry, A.: Lazy evaluation and delimited control. Log. Methods Comput. Sci. 6(3) (2010)","DOI":"10.2168\/LMCS-6(3:1)2010"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Une extension de L\u2019interpretation de g\u00f6del a L\u2019analyse, et son application a L\u2019elimination des coupures dans L\u2019analyse et la theorie des types. In: Fenstad, J.E., (ed.) Proceedings of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63\u201392. Elsevier (1971)","DOI":"10.1016\/S0049-237X(08)70843-7"},{"issue":"7","key":"15_CR12","doi-asserted-by":"publisher","first-page":"1269","DOI":"10.1017\/S0960129514000450","volume":"26","author":"M Guillermo","year":"2016","unstructured":"Guillermo, M., Miquel, A.: Specifying peirce\u2019s law in classical realizability. Math. Struct. Comput. Sci. 26(7), 1269\u20131303 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Guillermo, M., Miquey, \u00c9.: Classical realizability and arithmetical formul\u00e6. Math. Struct. Comput. Sci. 1\u201340 (2016)","DOI":"10.1017\/S0960129515000559"},{"key":"15_CR14","unstructured":"Herbelin, H.: C\u2019est maintenant qu\u2019on calcule: au c\u0153ur de la dualit\u00e9. Habilitation thesis, University Paris 11, December 2005"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Herbelin, H.: A constructive proof of dependent choice, compatible with classical logic. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, 25\u201328 June 2012, pp. 365\u2013374. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.47"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-662-49630-5_25","volume-title":"Foundations of Software Science and Computation Structures","author":"D Kesner","year":"2016","unstructured":"Kesner, D.: Reasoning about call-by-need by means of types. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 424\u2013441. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_25"},{"key":"15_CR17","series-title":"Ellis Horwood series in computers and their applications","volume-title":"Lambda-calculus, Types and Models","author":"J-L Krivine","year":"1993","unstructured":"Krivine, J.-L.: Lambda-calculus, Types and Models. Ellis Horwood series in computers and their applications. Ellis Horwood, Masson (1993)"},{"key":"15_CR18","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/S0304-3975(02)00776-4","volume":"308","author":"J-L Krivine","year":"2003","unstructured":"Krivine, J.-L.: Dependent choice, \u2018quote\u2019 and the clock. Theor. Comp. Sc. 308, 259\u2013276 (2003)","journal-title":"Theor. Comp. Sc."},{"key":"15_CR19","first-page":"197","volume":"27","author":"J-L Krivine","year":"2009","unstructured":"Krivine, J.-L.: Realizability in classical logic. Panoramas et synth\u00e8ses 27, 197\u2013229 (2009). Interactive models of computation and program behaviour","journal-title":"Panoramas et synth\u00e8ses"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Krivine, J.-L.: Realizability algebras: a program to well order r. Log. Methods Comput. Sci. 7(3) (2011)","DOI":"10.2168\/LMCS-7(3:2)2011"},{"issue":"1:10","key":"15_CR21","first-page":"1","volume":"8","author":"J-L Krivine","year":"2012","unstructured":"Krivine, J.-L.: Realizability algebras II: new models of ZF + DC. Log. Methods Comput. Sci. 8(1:10), 1\u201328 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"15_CR22","unstructured":"Krivine, J.-L.: On the structure of classical realizability models of ZF (2014)"},{"key":"15_CR23","unstructured":"Lafont, Y., Reus, B., Streicher, T.: Continuations semantics or expressing implication by negation. Technical report 9321, Ludwig-Maximilians-Universit\u00e4t, M\u00fcnchen (1993)"},{"issue":"3","key":"15_CR24","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10990-007-9013-1","volume":"20","author":"F Lang","year":"2007","unstructured":"Lang, F.: Explaining the lazy Krivine machine using explicit substitution and addresses. High.-Order Symbolic Comput. 20(3), 257\u2013270 (2007)","journal-title":"High.-Order Symbolic Comput."},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-662-49498-1_19","volume-title":"Programming Languages and Systems","author":"R Lepigre","year":"2016","unstructured":"Lepigre, R.: A classical realizability model for a semantical value restriction. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 476\u2013502. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_19"},{"issue":"3","key":"15_CR26","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1017\/S0956796898003037","volume":"8","author":"J Maraist","year":"1998","unstructured":"Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275\u2013317 (1998)","journal-title":"J. Funct. Program."},{"issue":"2","key":"15_CR27","doi-asserted-by":"publisher","first-page":"188","DOI":"10.2168\/LMCS-7(2:2)2011","volume":"7","author":"A Miquel","year":"2011","unstructured":"Miquel, A.: Existential witness extraction in classical realizability and via a negative translation. Log. Methods Comput. Sci. 7(2), 188\u2013202 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"15_CR28","unstructured":"Miquey, \u00c9.: Classical realizability and side-effects. Ph.D. thesis, Universit\u00e9 Paris-Diderot, Universidad de la Rep\u00fablica (Uruguay) (2017)"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-642-04027-6_30","volume-title":"Computer Science Logic","author":"G Munch-Maccagnoni","year":"2009","unstructured":"Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 409\u2013423. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04027-6_30"},{"issue":"1","key":"15_CR30","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01019945","volume":"7","author":"C Okasaki","year":"1994","unstructured":"Okasaki, C., Lee, P., Tarditi, D.: Call-by-need and continuation-passing style. Lisp Symbolic Comput. 7(1), 57\u201382 (1994)","journal-title":"Lisp Symbolic Comput."},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/3-540-55460-2_27","volume-title":"Logic Programming","author":"M Parigot","year":"1992","unstructured":"Parigot, M.: Free deduction: an analysis of \u201ccomputations\u201d in classical logic. In: Voronkov, A. (ed.) RCLP -1990. LNCS, vol. 592, pp. 361\u2013380. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55460-2_27"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-44450-5_36","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science","author":"M Parigot","year":"2000","unstructured":"Parigot, M.: Strong normalization of second order symmetric $$\\lambda $$-calculus. In: Kapoor, S., Prasad, S. (eds.) FSTTCS 2000. LNCS, vol. 1974, pp. 442\u2013453. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44450-5_36"},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-662-49498-1_24","volume-title":"Programming Languages and Systems","author":"P-M P\u00e9drot","year":"2016","unstructured":"P\u00e9drot, P.-M., Saurin, A.: Classical by-need. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 616\u2013643. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_24"},{"issue":"2","key":"15_CR34","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"GD Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-24727-2_30","volume-title":"Foundations of Software Science and Computation Structures","author":"E Polonovski","year":"2004","unstructured":"Polonovski, E.: Strong normalization of $$\\overline{\\lambda }\\mu \\widetilde{\\mu }$$-calculus with explicit substitutions. In: Walukiewicz, I. (ed.) FoSSaCS 2004. LNCS, vol. 2987, pp. 423\u2013437. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24727-2_30"},{"issue":"2","key":"15_CR36","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"WW Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symbolic Log. 32(2), 198\u2013212 (1967)","journal-title":"J. Symbolic Log."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89366-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T16:22:29Z","timestamp":1571156549000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89366-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319893655","9783319893662"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89366-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}