{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:17:31Z","timestamp":1762460251728},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319998398"},{"type":"electronic","value":"9783319998404"}],"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:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99840-4_12","type":"book-chapter","created":{"date-parts":[[2018,9,7]],"date-time":"2018-09-07T11:29:08Z","timestamp":1536319748000},"page":"205-225","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Uniform Strong Normalization for Multi-discipline Calculi"],"prefix":"10.1007","author":[{"given":"Paul","family":"Downen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philip","family":"Johnson-Freyd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zena M.","family":"Ariola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,8]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Ariola, Z.M., Herbelin, H., Saurin, A.: Classical call-by-need and duality. In: TLCA 2011 (2011)","DOI":"10.1007\/978-3-642-21691-6_6"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-57887-0_112","volume-title":"Theoretical Aspects of Computer Software","author":"F Barbanera","year":"1994","unstructured":"Barbanera, F., Berardi, S.: A symmetric lambda calculus for \u201cclassical\u201d program extraction. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 495\u2013515. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_112"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Curien, P.L., Herbelin, H.: The duality of computation. In: ICFP 2000 (2000)","DOI":"10.1145\/351240.351262"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-54833-8_14","volume-title":"Programming Languages and Systems","author":"P Downen","year":"2014","unstructured":"Downen, P., Ariola, Z.M.: The duality of construction. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 249\u2013269. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54833-8_14"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Downen, P., Johnson-Freyd, P., Ariola, Z.M.: Structures for structural recursion. In: ICFP 2015 (2015)","DOI":"10.1145\/2784731.2784762"},{"key":"12_CR6","unstructured":"Girard, J.Y.: Interpr\u00e9tation fonctionnelle et elimination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. These d\u2019\u00e9tat, Universit\u00e9 de Paris 7 (1972)"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR8","volume-title":"Proofs and Types","author":"JY Girard","year":"1989","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)"},{"key":"12_CR9","unstructured":"Graham-Lengrand, S.: Polarities & Focussing: a journey from Realisability to Automated Reasoning. Habilitation thesis, Universit\u00e9 Paris-Sud (2014)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical $$\\lambda $$\u03bb-calculus in \u201cnatural deduction\u201d form. In: TLCA 2009 (2009)","DOI":"10.1007\/978-3-642-02273-9_12"},{"issue":"4","key":"12_CR11","doi-asserted-by":"publisher","first-page":"109","DOI":"10.2307\/2269016","volume":"10","author":"SC Kleene","year":"1945","unstructured":"Kleene, S.C.: On the interpretation of intuitionistic number theory. J. Symbolic Logic 10(4), 109\u2013124 (1945)","journal-title":"J. Symbolic Logic"},{"issue":"3","key":"12_CR12","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10990-007-9018-9","volume":"20","author":"JL Krivine","year":"2007","unstructured":"Krivine, J.L.: A call-by-name lambda-calculus machine. High. Order Symbolic Comput. 20(3), 199\u2013207 (2007)","journal-title":"High. Order Symbolic Comput."},{"key":"12_CR13","unstructured":"Krivine, J.L.: Realizability in classical logic. In: Interactive models of computation and program behaviour, vol. 27. Soci\u00e9t\u00e9 Math\u00e9matique de France (2009)"},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.apal.2008.01.005","volume":"153","author":"S Lengrand","year":"2008","unstructured":"Lengrand, S., Miquel, A.: Classical F$$\\omega $$\u03c9, orthogonality and symmetric candidates. Ann. Pure Appl. Logic 153(1), 3\u201320 (2008)","journal-title":"Ann. Pure Appl. Logic"},{"key":"12_CR15","unstructured":"Levy, P.B.: Call-By-Push-Value. Ph.D. thesis, University of London, August 2001"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Liskov, B.: Keynote address-data abstraction and hierarchy. In: OOPSLA 1987 (1987)","DOI":"10.1145\/62138.62141"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Munch-Maccagnoni, G.: Focalisation and classical realisability. In: CSL 2009 (2009)","DOI":"10.1007\/978-3-642-04027-6_30"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Munch-Maccagnoni, G.: Syntax and Models of a non-Associative Composition of Programs and Proofs. Ph.D. thesis, Universit\u00e9 Paris Diderot (2013)","DOI":"10.1007\/978-3-642-54830-7_26"},{"key":"12_CR19","unstructured":"Peyton Jones, S.: https:\/\/www.red-gate.com\/simple-talk\/opinion\/geek-of-the-week\/simon-peyton-jones-geek-of-the-week\/"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Peyton Jones, S.L., Launchbury, J.: Unboxed values as first class citizens in a non-strict functional language. In: FPCA, pp. 636\u2013666 (1991)","DOI":"10.1007\/3540543961_30"},{"issue":"3","key":"12_CR21","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1017\/S0960129500003066","volume":"10","author":"AM Pitts","year":"2000","unstructured":"Pitts, A.M.: Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10(3), 321\u2013359 (2000)","journal-title":"Math. Struct. Comput. Sci."},{"key":"12_CR22","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. Theoret. Comput. Sci. 1, 125\u2013159 (1975)","journal-title":"Theoret. Comput. Sci."},{"key":"12_CR23","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-10394-4","volume-title":"The Parametric $$\\lambda $$\u03bb-Calculus: A Metamodel for Computation","author":"S Ronchi Della Rocca","year":"2004","unstructured":"Ronchi Della Rocca, S., Paolini, L.: The Parametric $$\\lambda $$\u03bb-Calculus: A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-10394-4"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: LFP 1992, pp. 288\u2013298 (1992)","DOI":"10.1145\/141478.141563"},{"key":"12_CR25","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 Logic 32, 198\u2013212 (1967)","journal-title":"J. Symbolic Logic"},{"key":"12_CR26","unstructured":"Turbak, F., Gifford, D., Sheldon, M.A.: Design Concepts in Programming Languages. The MIT Press (2008)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: FPCA 1989 (1989)","DOI":"10.1145\/99370.99404"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Call-by-value is dual to call-by-name. In: ICFP 2003 (2003)","DOI":"10.1145\/944705.944723"},{"issue":"1","key":"12_CR29","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A Wright","year":"1994","unstructured":"Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994)","journal-title":"Inf. Comput."},{"key":"12_CR30","unstructured":"Zeilberger, N.: The logical basis of evaluation order and pattern-matching. Ph.D. thesis, Carnegie Mellon University (2009)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99840-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T22:26:04Z","timestamp":1571869564000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99840-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319998398","9783319998404"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99840-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}