{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T14:10:02Z","timestamp":1751983802367,"version":"3.41.2"},"reference-count":75,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1999,9,1]],"date-time":"1999-09-01T00:00:00Z","timestamp":936144000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,9,1]],"date-time":"1999-09-01T00:00:00Z","timestamp":936144000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order and Symbolic Computation"],"published-print":{"date-parts":[[1999,9]]},"DOI":"10.1023\/a:1010000206149","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T00:56:42Z","timestamp":1040605002000},"page":"125-170","source":"Crossref","is-referenced-by-count":26,"title":["CPS Translations and Applications: The Cube and Beyond"],"prefix":"10.1007","volume":"12","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[]},{"given":"Morten Heine B.","family":"S\u00f8rensen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"234969_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A. Compiling with Continuations. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511609619"},{"key":"234969_CR2","doi-asserted-by":"crossref","unstructured":"Augustsson, L. Cayenne: A programming language with dependent types. In Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming. Baltimore, Maryland, 1998, ACM Press, pp. 239\u2013250.","DOI":"10.1145\/289423.289451"},{"key":"234969_CR3","unstructured":"Barendregt, H.P. The Lambda Calculus--Its Syntax and Semantics. North-Holland, 1984."},{"key":"234969_CR4","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P. Lambda calculi with types. In Handbook of Logic in Computer Science, S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum (Eds.). Vol. 2, Oxford Science Publications, 1992, pp. 117\u2013309.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"234969_CR5","unstructured":"Barthe, G., Hatcliff, J., and S\u00f8rensen, M.H. CPS-translation and applications: The cube and beyond. In Proceedings of the Second ACM SIGPLAN Workshop on Continuations, O. Danvy (Ed.), number NS-96-13 in BRICS Notes, 1996, pp. 4\/1\u20134\/31."},{"key":"234969_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hatcliff, J., and S\u00f8rensen, M.H. A notion of classical pure type system. In Proceedings of the Thirteenth Annual Conference on the Mathematical Foundations of Programming Semantics, S. Brookes and M. Mislove (Eds.). Pittsburgh, Pennsylvania, March 1997. Electronic Notes in Theoretical Computer Science, vol. 6.","DOI":"10.1016\/S1571-0661(05)80170-7"},{"key":"234969_CR7","unstructured":"Barthe, G., Hatcliff, J., and S\u00f8rensen, M.H.Weak Normalization Implies Strong Normalization in Generalized Non-Dependent Pure Type Systems. March 1997, submitted for publication."},{"key":"234969_CR8","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hatcliff, J., and S\u00f8rensen, M.H. Reflections on reflections. In Proceedings of the Ninth International Symposium on Programming Languages, Implementations, Logics and Programs, H. Glaser, P. Hartel, and H. Kuchen (Eds.). Southampton, United Kingdom, September 1997. Lecture Notes in Computer Science, vol. 1292, Springer-Verlag, pp. 241\u2013258.","DOI":"10.1007\/BFb0033848"},{"key":"234969_CR9","unstructured":"Barthe, G., Hatcliff, J., and S\u00f8rensen, M.H. An Induction Principle for Pure Type Systems. March 1998, submitted for publication."},{"key":"234969_CR10","unstructured":"Barthe, G., Hatcliff, J., and S\u00f8rensen, M.H. A taxonomy of CPS and DS translations. Technical Report TR 98-11, Department of Computing and Information Sciences, Kansas State University, 1988."},{"key":"234969_CR11","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hatcliff, J., and Thiemann, P. Monadic type systems: Pure type systems for impure settings. In Proceedings of the Second Workshop on Higher-Order Operational Techniques in Semantics (HOOTS II), A. Gordon, A. Pitts, and C. Talcott (Eds.). Stanford, California, December 1997. Electronic Notes in Theoretical Computer Science, vol. 10.","DOI":"10.1016\/S1571-0661(05)80691-7"},{"key":"234969_CR12","doi-asserted-by":"crossref","unstructured":"Barthe, G. and S\u00f8rensen, M.H. Domain-free pure type systems. In Proceedings of Logical Foundations of Computer Science LFCS'97, S. Adian and A. Nerode (Eds.), Yaroslav, Russia, July 1997. Lecture Notes in Computer Science, vol. 1234, Springer-Verlag, pp. 9\u201320.","DOI":"10.1007\/3-540-63045-7_2"},{"key":"234969_CR13","unstructured":"Berardi, S. Type Dependence and Constructive Mathematics. Ph.D. Thesis. University of Torino, 1990."},{"key":"234969_CR14","doi-asserted-by":"crossref","unstructured":"Consel, C. and Danvy, O. For a better support of static data flow. In Conference on Functional Programming and Computer Architecture, J. Hughes (Ed.). 1991. Lecture Notes in Computer Science, vol. 523, Springer-Verlag, pp. 495\u2013519.","DOI":"10.1007\/3540543961_24"},{"issue":"1","key":"234969_CR15","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1017\/S0956796800000952","volume":"4","author":"T. Coquand","year":"1994","unstructured":"Coquand, T. and Herbelin, H. A-translation and looping combinators in pure type systems. Journal of Functional Programming, 4(1):77\u201388, 1994.","journal-title":"Journal of Functional Programming"},{"key":"234969_CR16","unstructured":"Curry, H.B. and Feys, R. Combinatory Logic. North-Holland, 1958."},{"issue":"3","key":"234969_CR17","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0167-6423(94)00003-4","volume":"22","author":"O. Danvy","year":"1994","unstructured":"Danvy, O. Back to direct style. Science of Computer Programming, 22(3):183\u2013195, 1994.","journal-title":"Science of Computer Programming"},{"issue":"4","key":"234969_CR18","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O. Danvy","year":"1992","unstructured":"Danvy, O. and Filinski, A. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361\u2013391, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"234969_CR19","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1145\/141471.141564","volume":"V","author":"O. Danvy","year":"1992","unstructured":"Danvy, O. and Lawall, J. Back to direct style II: First-class continuations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming. San Francisco, California, June 1992. ACM Press, LISP Pointers, V(1):299\u2013310.","journal-title":"Proceedings of the 1992 ACM Conference on Lisp and Functional Programming"},{"key":"234969_CR20","first-page":"115","volume-title":"Informal Proceedings of TYPES'93","author":"G. Dowek","year":"1993","unstructured":"Dowek, G., Huet, G., and Werner, B. On the existence of long \u03b2\u03b7-normal forms in the cube. In Informal Proceedings of TYPES'93, H. Geuvers (Ed.). Nijmegen, The Netherlands, May 1993, pp. 115\u2013130."},{"key":"234969_CR21","doi-asserted-by":"crossref","unstructured":"Dussart, D., Hughes, J., and Thiemann, P. Type specialisation for imperative languages. In Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming. Amsterdam, The Netherlands, June 1997. ACM Press, pp. 204\u2013216.","DOI":"10.1145\/258948.258968"},{"key":"234969_CR22","unstructured":"Felleisen, M. The Calculi of \u03bb\n\n                    \u03c5\n                  -CS Conversion: A Syntactic Theory of Control and State in Imperative Higher Order Programming Languages. Ph.D. Thesis. Indiana University, 1987."},{"key":"234969_CR23","unstructured":"Felleisen, M. and Friedman, D. Control operators, the SECD machine, and the \u03bb;-calculus. In Formal Description of Programming Concepts III, M. Wirsing (Ed.), North-Holland, 1986, pp. 193\u2013217."},{"issue":"3","key":"234969_CR24","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","volume":"52","author":"M. Felleisen","year":"1987","unstructured":"Felleisen, M., Friedman, D., Kohlbecker, E., and Duba, B.Asyntactic theory of sequential control. Theoretical Computer Science, 52(3):205\u2013237, 1987.","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"234969_CR25","first-page":"237","volume":"28","author":"C. Flanagan","year":"1993","unstructured":"Flanagan, C., Sabry, A., Duba, B., and Felleisen, M. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation. Albuquerque, New Mexico, June 1993, pp. 237\u2013247, SIGPLAN Notices 28(6).","journal-title":"Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation"},{"key":"234969_CR26","unstructured":"Friedman, D., Wand, M., and Haynes, C. Essentials of Programming Languages. MIT Press and McGraw-Hill, 1991."},{"key":"234969_CR27","unstructured":"Gandy, R.O. An early proof of normalization by A.M. Turing. In J.P. Seldin and J.R. Hindley, Academic Press Limited, 1980, pp. 453\u2013455."},{"key":"234969_CR28","unstructured":"Geuvers, H. Logics and Type Systems. Ph.D. Thesis. University of Nijmegen, 1993."},{"key":"234969_CR29","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Geuvers, H. and Nederhof, M.J. A modular proof of strong normalisation for the Calculus of Constructions. Journal of Functional Programming, 1:155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"key":"234969_CR30","unstructured":"Girard, J.-Y. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur. Th\u00e8se d'Etat. Universit\u00e9 Paris VII, 1972."},{"key":"234969_CR31","doi-asserted-by":"crossref","unstructured":"Griffin, T.G. A formulae-as-types notion of control. In Conference Record of the Annual ACM Symposium on Principles of Programming Languages. San Francisco, California, January 1990. ACM Press, pp. 47\u201358.","DOI":"10.1145\/96709.96714"},{"key":"234969_CR32","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/BFb0037105","volume-title":"Typed Lambda Calculus and Applications","author":"P. de Groote","year":"1993","unstructured":"de Groote, P. The conservation theorem revisited. In Typed Lambda Calculus and Applications, M. Bezem and J.F. Groote (Eds.). Utrecht, The Netherlands, March 1993. Lecture Notes in Computer Science, vol. 664, Springer-Verlag, pp. 163\u2013178."},{"issue":"1","key":"234969_CR33","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., and Plotkin, G. A framework for defining logics. Journal of the ACM, 40(1):143\u201384, 1993.A PreliminaryVersion Appeared in the Proceedings of the First IEEE Symposium on Logic in Computer Science, June 1987, pp. 194\u2013204.","journal-title":"Journal of the ACM"},{"key":"234969_CR34","doi-asserted-by":"crossref","unstructured":"Harper, R. and Lillibridge, M. Explicit polymorphism and CPS conversion. In Conference Record of the Twentieth Annual ACM Symposium on Principles of Programming Languages. Charleston, South Carolina, January 1993, ACM Press, pp. 206\u2013219.","DOI":"10.1145\/158511.158630"},{"key":"234969_CR35","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BF01019463","volume":"6","author":"R. Harper","year":"1993","unstructured":"Harper, R. and Lillibridge, M. Polymormphic type assignment and CPS conversion. LISP and Symbolic Computation, 6:361\u2013380, 1993.","journal-title":"LISP and Symbolic Computation"},{"issue":"2","key":"234969_CR36","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1145\/169701.169696","volume":"15","author":"R. Harper","year":"1993","unstructured":"Harper, R. and Mitchell, J.C. On the type structure of Standard ML. ACM Transactions on Programming Languages and Systems, 15(2):211\u2013252, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"234969_CR37","doi-asserted-by":"crossref","unstructured":"Harper, R. and Morrisett, G. Compiling polymorphism using intensional type analysis. In Conference Record of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages. San Francisco, California, January 1995, ACM Press, pp. 130\u2013141.","DOI":"10.1145\/199448.199475"},{"key":"234969_CR38","doi-asserted-by":"crossref","unstructured":"Hatcliff, J. Foundations of partial evaluation of functional programs with computational effects. In Symposium on Partial Evaluation, O. Danvy, R. Gl\u00fcck, and P. Thiemann (Eds.). September 1998 ACM Computing Surveys, vol. 30.","DOI":"10.1145\/289121.289134"},{"key":"234969_CR39","doi-asserted-by":"crossref","unstructured":"Hatcliff, J. and Danvy, O. A generic account of continuation-passing styles. In Conference Record of the Twenty-First Annual ACM Symposium on Principles of Programming Languages. Portland, Oregon, January 1994, ACM Press, pp. 458\u2013471.","DOI":"10.1145\/174675.178053"},{"key":"234969_CR40","doi-asserted-by":"crossref","first-page":"507","DOI":"10.1017\/S0960129597002405","volume":"7","author":"J. Hatcliff","year":"1997","unstructured":"Hatcliff, J. and Danvy, O. A computational formalization for partial evaluation. Mathematical Structures in Computer Science, 7:507\u2013541, 1997. Special issue devoted to selected papers from the Workshop on Logic, Domains, and Programming Languages. Darmstadt, Germany, May 1995.","journal-title":"Mathematical Structures in Computer Science"},{"key":"234969_CR41","unstructured":"Hindley, J.R. and Seldin, J.P. Introduction to Combinators and \u03bb-Calculus. Cambridge University Press, 1986."},{"key":"234969_CR42","unstructured":"Howard, W. The formulae-as-types notion of construction. In T.H.B. Curry: Essays on Combinatory Logic, Lambda, Calculus and Formalism, J.P. Seldin and J.R. Hindley, Academic Press Limited, 1980, pp. 479\u2013490."},{"key":"234969_CR43","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/BFb0014551","volume-title":"Proceedings of Theoretical Aspects of Computer Software","author":"J. Lawall","year":"1997","unstructured":"Lawall, J. and Thiemann, P. Sound specialization in the presence of computational effects. In Proceedings of Theoretical Aspects of Computer Software, M. Abadi and T. Ito (Eds.). Sendai, Japan, September 1997. Lecture Notes in Computer Science, vol. 1281, Springer-Verlag, pp. 165\u2013190."},{"issue":"2","key":"234969_CR44","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1017\/S0960129500001298","volume":"1","author":"G. Longo","year":"1991","unstructured":"Longo, G. and Moggi, E. Constructive natural deduction and its \u2018\u03ce-set\u2019 interpretation. Mathematical Structures in Computer Science, 1(2):215\u2013254, 1991.","journal-title":"Mathematical Structures in Computer Science"},{"key":"234969_CR45","unstructured":"Meijer, E. and Peyton Jones, S. Henk: A typed intermediate language. In Proceedings of the ACM SIGPLAN Workshop on Types in Compilation, Amsterdam, The Netherlands, June 1997."},{"key":"234969_CR46","doi-asserted-by":"crossref","unstructured":"Meyer, A.R. and Wand, M. Continuation semantics in typed lambda-calculi (summary). In Logics of Programs, R. Parikh (Ed.). Lecture Notes in Computer Science, vol. 193, Springer-Verlag, 1985, pp. 219\u2013224.","DOI":"10.1007\/3-540-15648-8_17"},{"key":"234969_CR47","doi-asserted-by":"crossref","unstructured":"Minamide, Y., Morrisett, G., and Harper, R. Typed closure conversion. In Conference Record of the Twentythird Annual ACM Symposium on Principles of Programming Languages. St. Petersburg, Florida, January 1996, ACM Press, pp. 271\u2013283.","DOI":"10.1145\/237721.237791"},{"key":"234969_CR48","unstructured":"Murthy, C. Extracting Constructive Contents from Classical Proofs. Ph.D. Thesis, Cornell University, 1990."},{"key":"234969_CR49","doi-asserted-by":"crossref","unstructured":"Nielsen, K. and S\u00f8rensen, M.H. Call-by-name CPS-translation as a binding-time improvement. In Static Analysis Symposium, A. Mycroft (Ed.). Glasgow, Scotland, September 1995. Lecture Notes in Computer Science, Springer-Verlag, vol. 983, pp. 296\u2013313.","DOI":"10.1007\/3-540-60360-3_46"},{"key":"234969_CR50","unstructured":"Peyton Jones, S.L. The Implementation of Functional Programming Languages. Prentice Hall International. 1987."},{"key":"234969_CR51","unstructured":"Peyton Jones, S.L., Hall, C., Hammond, K., Partain, W., and Wadler, P. The Glasgow Haskell compiler: A technical overview. In Proceedings of the UK Joint Framework for Information Technology (JFIT) Technical Conference, Keele, 1993."},{"key":"234969_CR52","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G. Plotkin","year":"1975","unstructured":"Plotkin, G. Call-by-name, call-by-value and the \u03bb-calculus. Theoretical Computer Science, 1:125\u2013159, 1975.","journal-title":"Theoretical Computer Science"},{"key":"234969_CR53","unstructured":"Prawitz, D. Natural Deduction: A Proof Theoretical Study. Almquist & Wiksell, 1965."},{"key":"234969_CR54","doi-asserted-by":"crossref","unstructured":"Prawitz, D. Ideas and results of proof theory. In The 2nd Scandinavian Logical Symposium, J.E. Fenstad (Ed.). North-Holland, 1970, pp. 235\u2013307.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"234969_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1007\/3-540-57887-0_113","volume-title":"Theoretical Aspects of Computer Software","author":"N.J. Rehof","year":"1994","unstructured":"Rehof, N.J. and S\u00f8rensen, M.H. The \u03bb\u0394 calculus. In Theoretical Aspects of Computer Software, M. Hagiya and J. Mitchell (Eds.). Sendai, Japan, April 1994. Lecture Notes in Computer Science, vol. 789, Springer-Verlag, pp. 516\u2013542."},{"issue":"4","key":"234969_CR56","first-page":"7","volume":"11","author":"J.C. Reynolds","year":"1998","unstructured":"Reynolds, J.C. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation\n11(4):7\u2013105, 1998. Reprinted from the proceedings of the 25thACMNational Conference, 1972.","journal-title":"Higher-Order and Symbolic Computation"},{"key":"234969_CR57","unstructured":"Sabry, A. Note on Axiomatizing the Semantics of Control Operators. Technical Report CIS-TR-96-03. Department of Computer and Information Science, University of Oregon, 1996."},{"key":"234969_CR58","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/BF01019462","volume":"6","author":"A. Sabry","year":"1993","unstructured":"Sabry, A. and Felleisen, M. Reasoning about programs in continuation-passing style. Lisp and Symbolic Computation, 6:289\u2013360, 1993.","journal-title":"Lisp and Symbolic Computation"},{"issue":"6","key":"234969_CR59","first-page":"1","volume":"29","author":"A. Sabry","year":"1994","unstructured":"Sabry, A. and Felleisen, M. Is continuation passing useful for data-flow analysis? In Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation, Orlando, Florida, June 1994, pp. 1\u201312. SIGPLAN Notices 29(6).","journal-title":"Proceedings of the ACM SIGPLAN'94 Conference on Programming Language Design and Implementation, Orlando, Florida"},{"issue":"6","key":"234969_CR60","doi-asserted-by":"crossref","first-page":"916","DOI":"10.1145\/267959.269968","volume":"19","author":"A. Sabry","year":"1997","unstructured":"Sabry, A. and Wadler, P. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916\u2013941, 1997. Earlier version in the proceedings of the 1996 International Conference on Functional Programming.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"234969_CR61","unstructured":"Schmidt, D.A. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, Inc., 1986."},{"issue":"2","key":"234969_CR62","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF02770512","volume":"XLVIII","author":"J.P. Seldin","year":"1989","unstructured":"Seldin, J.P. Normalization and excluded middle I. Studia Logica, XLVIII(2):193\u2013217, 1989.","journal-title":"Studia Logica"},{"key":"234969_CR63","unstructured":"Seldin, J.P. and Hindley, J.R. (Eds.). To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press Limited, 1980."},{"issue":"6","key":"234969_CR64","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/207110.207123","volume":"30","author":"Z. Shao","year":"1995","unstructured":"Shao, Z. and Appel, A.W. A type-based compiler for Standard ML. In Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation, La Jolla, California, June 1995, pp. 116\u2013129, SIGPLAN Notices 30(6).","journal-title":"Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation, La Jolla, California"},{"key":"234969_CR65","unstructured":"Shivers, O. Control-Flow Analysis of Higher-Order Languages. Ph.D. Thesis. Carnegie Mellon University, 1991."},{"issue":"1","key":"234969_CR66","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1996.2622","volume":"133","author":"M.H. S\u00f8rensen","year":"1997","unstructured":"S\u00f8rensen, M.H. Strong normalization from weak normalization in typed \u03bb-calculi. Information and Computation, 133(1):35\u201371, 1997.","journal-title":"Information and Computation"},{"issue":"1","key":"234969_CR67","doi-asserted-by":"crossref","first-page":"129","DOI":"10.2307\/2274910","volume":"56","author":"G. St\u00e5lmarck","year":"1991","unstructured":"St\u00e5lmarck, G. Normalization theorems for full first order classical natural deduction. Journal of Symbolic Logic, 56(1):129\u2013149, 1991.","journal-title":"Journal of Symbolic Logic"},{"key":"234969_CR68","series-title":"Technical Report","volume-title":"Rabbit: A compiler for scheme","author":"G.L. Steele Jr.","year":"1978","unstructured":"Steele, G.L., Jr. Rabbit: A compiler for scheme. Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, May 1978."},{"issue":"2","key":"234969_CR69","doi-asserted-by":"crossref","first-page":"190","DOI":"10.2307\/2271656","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):190\u2013212, 1967.","journal-title":"Journal of Symbolic Logic"},{"key":"234969_CR70","doi-asserted-by":"crossref","unstructured":"Tait, W.W. Arealizability interpretation of the theory of species. In Logic Colloquium, R. Parikh (Ed.). Lecture Notes in Mathematics, vol. 453, Springer-Verlag, 1975, pp. 240\u2013251.","DOI":"10.1007\/BFb0064875"},{"issue":"5","key":"234969_CR71","first-page":"181","volume":"31","author":"D. Tarditi","year":"1996","unstructured":"Tarditi, D., Morrisett, G., Cheng, P., Stone, C., Harper, R., and Lee, P. TIL: A type-directed optimizing compiler for ML. In Proceedings of the ACM SIGPLAN' 96 Conference on Programming Language Design and Implementation, Philadelphia, Pennsylvania, May 1996, pp. 181\u2013192. SIGPLAN Notices 31(5).","journal-title":"Proceedings of the ACM SIGPLAN' 96 Conference on Programming Language Design and Implementation, Philadelphia, Pennsylvania"},{"key":"234969_CR72","unstructured":"Terlouw, J. Een Nadere Bewijstheoretische Analyse van GSTT's. Manuscript (in Dutch), 1989."},{"key":"234969_CR73","unstructured":"Werner, B. Continuations, Evaluation Styles and Types Systems. Manuscript, 1992."},{"key":"234969_CR74","doi-asserted-by":"crossref","unstructured":"Xi, H. Weak and strong normalizations in typed \u03bb-calculi. In Proceedings of TLCA'97, P. de Groote and J. Hindley (Eds.). Nancy, France, Lecture Notes in Computer Science, vol. 1210, Springer-Verlag, April 1997, pp. 390\u2013404.","DOI":"10.1007\/3-540-62688-3_48"},{"issue":"5","key":"234969_CR75","first-page":"249","volume":"33","author":"H. Xi","year":"1998","unstructured":"Xi, H. and Pfenning, F. Eliminating array bound checking through dependent types. In Proceedings of the ACM SIGPLAN'98 Conference on Programming Languages Design and Implementation, Montr\u00e9al, Canada, June 1998, pp. 249\u2013257. SIGPLAN Notices 33(5).","journal-title":"Proceedings of the ACM SIGPLAN'98 Conference on Programming Languages Design and Implementation, Montr\u00e9al, Canada"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010000206149.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1010000206149\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1010000206149.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T13:49:58Z","timestamp":1751982598000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1010000206149"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,9]]},"references-count":75,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,9]]}},"alternative-id":["234969"],"URL":"https:\/\/doi.org\/10.1023\/a:1010000206149","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"type":"print","value":"1388-3690"},{"type":"electronic","value":"1573-0557"}],"subject":[],"published":{"date-parts":[[1999,9]]}}}