{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:12:34Z","timestamp":1725664354777},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581406"},{"type":"electronic","value":"9783540484424"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58140-5_15","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:18:29Z","timestamp":1330269509000},"page":"142-152","source":"Crossref","is-referenced-by-count":1,"title":["Strong normalization in a non-deterministic typed lambda-calculus"],"prefix":"10.1007","author":[{"given":"Philippe de","family":"Groote","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"15_CR1","unstructured":"H.P. Barendregt. The lambda calculus, its syntax and semantics. North-Holland, revised edition, 1984."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"R. Constable and C. Murthy. Finding computational content in classical proofs. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 341\u2013362. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.014"},{"key":"15_CR3","unstructured":"H.B. Curry and R. Feys. Combinatory Logic, Vol. I. North-Holland, 1958."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Ph. de Groote. Denotations for classical proofs \u2014 preliminary results. In A. Nerode and M. Taitslin, editors, Proceedings of the Second International Symposium on Logical Foundations of Computer Science \u2014 Tver'92, pages 105\u2013116. Lecture Notes in Computer Science, 620, Springer Verlag, 1992.","DOI":"10.1007\/BFb0023867"},{"key":"15_CR5","unstructured":"M.C. Fitting. Intuitionistic Logic Model Theory and Forcing. North Holland Publishing Company, 1969."},{"key":"15_CR6","unstructured":"J.H. Gallier. Logic for Computer Science. John Wiley & Sons, 1988."},{"key":"15_CR7","unstructured":"J.H. Gallier. On Girard's \u201cCandidats de R\u00e9ductibilit\u00e9\u201d. In P. Odifreddi, editor, Logic and Computer Science, pages 123\u2013203. Academic Press, 1990."},{"key":"15_CR8","unstructured":"J.H. Gallier. On the correspondence between proofs and \u03bb-terms. In Cahiers du Centre de Logique, Volume 8. Universit\u00e9 Catholique de Louvain, to appear."},{"key":"15_CR9","unstructured":"G. Gentzen. Recherches sur la d\u00e9duction logique (Untersuchungen \u00fcber das logische schliessen). Presses Universitaires de France, 1955. Traduction et commentaire par R. Feys et J. Ladri\u00e8re."},{"key":"15_CR10","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"J.-Y. Girard. A new constructive logic: Classical logic. Mathematical Structures in Computer Science, 1:255\u2013296, 1991.","journal-title":"Mathematical Structures in Computer Science"},{"key":"15_CR11","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"T. G. Griffin. A formulae-as-types notion of control. In Conference record of the seventeenth annual ACM symposium on Principles of Programming Languages, pages 47\u201358, 1990.","DOI":"10.1145\/96709.96714"},{"key":"15_CR13","unstructured":"J.R. Hindley and J.P. Seldin. Introduction to combinators and \u03bb-calculus. London Mathematical Society Student Texts. Cambridge University Press, 1986."},{"key":"15_CR14","unstructured":"W.A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479\u2013490. Academic Press, 1980."},{"key":"15_CR15","unstructured":"S.C. Kleene. Introduction to metamathematics. North-Holland Publishing Company, 1954. Sixth Reprint (1971)."},{"volume-title":"Mathematical Logic and Hilbert's \u03b5-Symbol","year":"1969","author":"A.C. Leisenring","key":"15_CR16","unstructured":"A.C. Leisenring. Mathematical Logic and Hilbert's \u03b5-Symbol. Gordon and Breach Science Publishers, New-York, 1969."},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"C. R. Murthy. An evaluation semantics for classical proofs. In Proceedings of the sixth annual IEEE symposium on logic in computer science, pages 96\u2013107, 1991.","DOI":"10.1109\/LICS.1991.151634"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"C. R. Murthy. A computational analysis of Girard's translation and LC. In Proceedings of the seventh annual IEEE symposium on logic in computer science, pages 90\u2013101, 1992.","DOI":"10.1109\/LICS.1992.185523"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"M. Parigot. \u03bb\u03bc-Calculus: an algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 190\u2013201. Lecture Notes in Artificial Intelligence, 624, Springer Verlag, 1992.","DOI":"10.1007\/BFb0013061"},{"volume-title":"Natural Deduction, A Proof-Theoretical Study","year":"1965","author":"D. Prawitz","key":"15_CR20","unstructured":"D. Prawitz. Natural Deduction, A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm, 1965."},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"S. Stenlund. Combinators \u03bb-terms and proof theory. D. Reidel Publishing Company, 1972.","DOI":"10.1007\/978-94-010-2913-1"}],"container-title":["Lecture Notes in Computer Science","Logical Foundations of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58140-5_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:13Z","timestamp":1605647833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58140-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581406","9783540484424"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-58140-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}