{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T02:10:09Z","timestamp":1744078209141,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642334740"},{"type":"electronic","value":"9783642334757"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33475-7_26","type":"book-chapter","created":{"date-parts":[[2012,9,8]],"date-time":"2012-09-08T06:43:09Z","timestamp":1347086589000},"page":"372-387","source":"Crossref","is-referenced-by-count":2,"title":["An Output-Based Semantics of \u039b\u03bc with Explicit Substitution in the \u03c0-Calculus"],"prefix":"10.1007","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maria Grazia","family":"Vigliotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"26_CR1","first-page":"375","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit Substitutions. JFP\u00a01(4), 375\u2013416 (1991)","journal-title":"JFP"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus. In: CCS 1997, pp. 36\u201347 (1997)","DOI":"10.1145\/266420.266432"},{"key":"26_CR3","unstructured":"Abramsky, S.: The lazy lambda calculus. Research topics in functional programming, pp. 65\u2013116. Addison-Wesley (1990)"},{"key":"26_CR4","unstructured":"Audebaud, P.: Explicit Substitutions for the \u039b\u03bc Calculus. RR\u00a094-26, \u00c9NS de Lyon (1994)"},{"key":"26_CR5","doi-asserted-by":"publisher","first-page":"1400","DOI":"10.1016\/j.apal.2010.04.010","volume":"161","author":"S. Bakel van","year":"2010","unstructured":"van Bakel, S.: Completeness and Partial Soundness Results for Intersection & Union Typing for $\\bar{\\lambda}{\\mu}{\\tilde{\\mu}}$ . Annals of Pure and Applied Logic\u00a0161, 1400\u20131430 (2010)","journal-title":"Annals of Pure and Applied Logic"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"van Bakel, S.: Completeness and Soundness results for $\\cal X$ with Intersection and Union Types. Fundamenta Informaticae (to appear, 2012)","DOI":"10.3233\/FI-2012-770"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-21691-6_18","volume-title":"Typed Lambda Calculi and Applications","author":"S. Bakel van","year":"2011","unstructured":"van Bakel, S., Barbanera, F., de\u2019Liguoro, U.: A Filter Model for the \u03bb\u03bc-Calculus. In: Ong, L. (ed.) TLCA 2011. LNCS, vol.\u00a06690, pp. 213\u2013228. Springer, Heidelberg (2011)"},{"key":"26_CR8","unstructured":"van Bakel, S., Cardelli, L., Vigliotti, M.G.: From $\\cal X$ to \u03c0; Representing the Classical Sequent Calculus in the \u03c0-calculus. In: CL&C 2008 (2008)"},{"key":"26_CR9","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":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04081-8_7","volume-title":"CONCUR 2009 - Concurrency Theory","author":"S. Bakel van","year":"2009","unstructured":"van Bakel, S., Vigliotti, M.G.: A Logical Interpretation of the \u03bb-Calculus into the \u03c0-Calculus, Preserving Spine Reduction and Types. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 84\u201398. Springer, Heidelberg (2009)"},{"key":"26_CR11","unstructured":"Barendregt, H.: The Lambda Calculus: its Syntax and Semantics. North-Holland (1984)"},{"key":"26_CR12","unstructured":"Bloo, R., Rose, K.H.: Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection. In: CSN 1995, pp. 62\u201372 (1995)"},{"key":"26_CR13","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda Calculus Notation with Nameless Dummies: A Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem. Ind.\u00a0Math.\u00a034, 381\u2013392 (1972)","journal-title":"Ind.\u00a0Math."},{"issue":"1","key":"26_CR14","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":"26_CR15","unstructured":"Cimini, M., Sacerdoti Coen, C., Sangiorgi, D.: $\\bar{\\lambda}{\\mu}{\\tilde{\\mu}}$ calculus, \u03c0-calculus, and abstract machines. In: EXPRESS 2009 (2009)"},{"issue":"6","key":"26_CR16","first-page":"625","volume":"9","author":"T. Crolard","year":"1999","unstructured":"Crolard, T.: A confluent lambda-calculus with a catch\/throw mechanism. JFP\u00a09(6), 625\u2013647 (1999)","journal-title":"JFP"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Herbelin, H.: The Duality of Computation. In: ICFP 2000, pp. 233\u2013243. ACM (2000)","DOI":"10.1145\/357766.351262"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, p. 68. North Holland (1935, 1969)","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-58216-9_27","volume-title":"Logic Programming and Automated Reasoning","author":"P. Groote de","year":"1994","unstructured":"de Groote, P.: On the Relation Between the \u03bb\u03bc-Calculus and the Syntactic Theory of Sequential Control. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol.\u00a0822, pp. 31\u201343. Springer, Heidelberg (1994)"},{"key":"26_CR20","unstructured":"Herbelin, H.: C\u2019est maintenant qu\u2019on calcule: au c\u0153ur de la dualit\u00e9. M\u00e9moire d\u2019habilitation, Universit\u00e9 Paris 11 (2005)"},{"key":"26_CR21","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":"26_CR22","unstructured":"Honda, K., Yoshida, N., Berger, M.: Control in the \u03c0-Calculus. In: CW 2004 (2004)"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Lassen, S.B.: Head Normal Form Bisimulation for Pairs and the \u03bb\u03bc-Calculus. In: LICS 2006, pp. 297\u2013306 (2006)","DOI":"10.1109\/LICS.2006.29"},{"issue":"2","key":"26_CR24","first-page":"269","volume":"2","author":"R. Milner","year":"1992","unstructured":"Milner, R.: Functions as processes. MSCS\u00a02(2), 269\u2013310 (1992)","journal-title":"MSCS"},{"key":"26_CR25","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":"26_CR26","doi-asserted-by":"crossref","unstructured":"Parigot, M.: Strong Normalization for Second Order Classical Natural Deduction. In: LICS 1993, pp. 39\u201346 (1993)","DOI":"10.1109\/LICS.1993.287602"},{"issue":"5","key":"26_CR27","first-page":"409","volume":"6","author":"B.C. Pierce","year":"1996","unstructured":"Pierce, B.C., Sangiorgi, D.: Typing and Subtyping for Mobile Processes. MSCS\u00a06(5), 409\u2013453 (1996)","journal-title":"MSCS"},{"key":"26_CR28","unstructured":"Py, W.: Confluence en \u03bb\u03bc-calcul. Phd thesis, Univ.\u00a0Savoie (1998)"},{"key":"26_CR29","unstructured":"Sangiorgi, D.: Expressing Mobility in Process Algebra: First Order and Higher Order Paradigms. PhD thesis, Univ. Edinburgh (1992)"},{"key":"26_CR30","unstructured":"Sangiorgi, D.: Lazy functions and mobile processes. RR 2515, INRIA, Sophia-Antipolis, France (1995)"},{"key":"26_CR31","unstructured":"Sangiorgi, D., Walker, D.: The Pi-Calculus. Cambridge University Press (2001)"},{"key":"26_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-36377-7_19","volume-title":"The Essence of Computation","author":"P. Sestoft","year":"2002","unstructured":"Sestoft, P.: Demonstrating Lambda Calculus Reduction. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 420\u2013435. Springer, Heidelberg (2002)"},{"key":"26_CR33","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1137\/0205036","volume":"5","author":"C.P. Wadsworth","year":"1976","unstructured":"Wadsworth, C.P.: The relation between computational and denotational properties for Scott\u2019s D\u2009\u221e\u2009-models of the lambda-calculus. SIAM JoC\u00a05, 488\u2013521 (1976)","journal-title":"SIAM JoC"}],"container-title":["Lecture Notes in Computer Science","Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33475-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,8]],"date-time":"2025-04-08T01:51:26Z","timestamp":1744077086000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33475-7_26"}},"subtitle":["Extended Abstract"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642334740","9783642334757"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33475-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}