{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T11:05:57Z","timestamp":1791111957151,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642040801","type":"print"},{"value":"9783642040818","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04081-8_7","type":"book-chapter","created":{"date-parts":[[2009,8,31]],"date-time":"2009-08-31T12:27:08Z","timestamp":1251721628000},"page":"84-98","source":"Crossref","is-referenced-by-count":8,"title":["A Logical Interpretation of the \u03bb-Calculus into the \u03c0-Calculus, Preserving Spine Reduction and Types"],"prefix":"10.1007","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maria Grazia","family":"Vigliotti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus. In: CC&CS 1997, pp. 36\u201347 (1997)","DOI":"10.1145\/266420.266432"},{"key":"7_CR2","unstructured":"Abramsky, S.: The lazy lambda calculus. In: Research topics in functional programming, pp. 65\u2013116 (1990)"},{"issue":"1","key":"7_CR3","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/0304-3975(94)00103-0","volume":"135","author":"S. Abramsky","year":"1994","unstructured":"Abramsky, S.: Proofs as Processes. TCS\u00a0135(1), 5\u20139 (1994)","journal-title":"TCS"},{"key":"7_CR4","unstructured":"van Bakel, S., Cardelli, L., Vigliotti, M.G.: From X to \u03c0; Representing the Classical Sequent Calculus in \u03c0-calculus. In: CL&C 2008 (2008)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11560586_8","volume-title":"Theoretical Computer Science","author":"S. Bakel van","year":"2005","unstructured":"van Bakel, S., Lengrand, S., Lescanne, P.: The language formula_image: Circuits, computations and classical logic. In: Coppo, M., Lodi, E., Pinna, G.M. (eds.) ICTCS 2005. LNCS, vol.\u00a03701, pp. 81\u201396. Springer, Heidelberg (2005)"},{"key":"7_CR6","first-page":"555","volume":"18","author":"S. Bakel van","year":"2008","unstructured":"van Bakel, S., Lescanne, P.: Computation with Classical Sequents. MSCS\u00a018, 555\u2013609 (2008)","journal-title":"MSCS"},{"key":"7_CR7","volume-title":"The Lambda Calculus: its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam (1984)"},{"issue":"3","key":"7_CR8","first-page":"191","volume":"75","author":"H.P. Barendregt","year":"1987","unstructured":"Barendregt, H.P., Kennaway, R., Klop, J.W., Sleep, M.R.: Needed Reduction and Spine Strategies for the Lambda Calculus. I&C\u00a075(3), 191\u2013231 (1987)","journal-title":"I&C"},{"issue":"1","key":"7_CR9","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0304-3975(94)00104-9","volume":"135","author":"G. Bellin","year":"1994","unstructured":"Bellin, G., Scott, P.J.: On the pi-Calculus and Linear Logic. TCS\u00a0135(1), 11\u201365 (1994)","journal-title":"TCS"},{"key":"7_CR10","unstructured":"Bloo, R., Rose, K.H.: Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection. In: CSN 1995 \u2013 Computer Science in the Netherlands, pp. 62\u201372 (1995)"},{"issue":"1","key":"7_CR11","first-page":"40","volume":"1","author":"A. Church","year":"1936","unstructured":"Church, A.: A note on the entscheidungsproblem. JSL\u00a01(1), 40\u201341 (1936)","journal-title":"JSL"},{"key":"7_CR12","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, p. 68, 1935. North Holland, Amsterdam (1969)"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das Logische Schliessen. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1935)","journal-title":"Mathematische Zeitschrift"},{"key":"7_CR14","unstructured":"Goubault-Larrecq, J.: A Few Remarks on SKInT. RR-3475, INRIA Rocquencourt (1998)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BFb0057019","volume-title":"ECOOP \u201991 European Conference on Object-Oriented Programming","author":"K. Honda","year":"1991","unstructured":"Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol.\u00a0512, pp. 133\u2013147. Springer, Heidelberg (1991)"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/0304-3975(95)00074-7","volume":"151","author":"K. Honda","year":"1995","unstructured":"Honda, K., Yoshida, N.: On the Reduction-based Process Semantics. TCS\u00a0151, 437\u2013486 (1995)","journal-title":"TCS"},{"key":"7_CR17","unstructured":"Honda, K., Yoshida, N., Berger, M.: Control in the \u03c0-Calculus. In: CW 2004 (2004)"},{"issue":"2","key":"7_CR18","first-page":"269","volume":"2","author":"R. Milner","year":"1992","unstructured":"Milner, R.: Function as processes. MSCS\u00a02(2), 269\u2013310 (1992)","journal-title":"MSCS"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M. Parigot","year":"1992","unstructured":"Parigot, M.: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624, pp. 190\u2013201. Springer, Heidelberg (1992)"},{"key":"7_CR20","unstructured":"Sangiorgi, D.: Expressing Mobility in Process Algebra: First Order and Higher order Paradigms. PhD thesis, Edinburgh University (1992)"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-58027-1_7","volume-title":"Mathematical Foundations of Programming Semantics","author":"D. Sangiorgi","year":"1994","unstructured":"Sangiorgi, D.: An Investigation into Functions as Processes. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol.\u00a0802, pp. 143\u2013159. Springer, Heidelberg (1994)"},{"key":"7_CR22","unstructured":"Sangiorgi, D.: Lazy functions and processes. RR2515, INRIA, Sophia-Antipolis (1995)"},{"key":"7_CR23","volume-title":"The Pi-Calculus","author":"D. Sangiorgi","year":"2003","unstructured":"Sangiorgi, D., Walker, D.: The Pi-Calculus. Cambridge University Press, Cambridge (2003)"},{"key":"7_CR24","unstructured":"Sestoft, P.: Standard ML on the Web server. Department of Mathematics and Physics, Royal Veterinary and Agricultural University, Denmark (1996)"},{"key":"7_CR25","unstructured":"Thielecke, H.: Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh (1997)"},{"key":"7_CR26","unstructured":"Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge (2000)"},{"issue":"1, 2","key":"7_CR27","first-page":"123","volume":"45","author":"C. Urban","year":"2001","unstructured":"Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. FI\u00a045(1, 2), 123\u2013155 (2001)","journal-title":"FI"},{"key":"7_CR28","unstructured":"de Vries, F.-J.: B\u00f6hm trees, bisimulations and observations in lambda calculus. In: FLP 1997, pp. 230\u2013245 (1997)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2009 - Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04081-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T04:47:08Z","timestamp":1558500428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04081-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040801","9783642040818"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04081-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}