{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:37:53Z","timestamp":1725489473764},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414131"},{"type":"electronic","value":"9783540444503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44450-5_36","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:26:08Z","timestamp":1187252768000},"page":"442-453","source":"Crossref","is-referenced-by-count":3,"title":["Strong Normalization of Second Order Symmetric \u03bb-Calculus"],"prefix":"10.1007","author":[{"given":"Michel","family":"Parigot","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,11,24]]},"reference":[{"key":"36_CR1","first-page":"103","volume-title":"Information and Computation","author":"F. Barbanera","year":"1996","unstructured":"F. Barbanera, S. Berardi: A symmetric lambda-calculus for classical program extraction. Information and Computation 125 (1996) 103\u2013117."},{"key":"36_CR2","unstructured":"F. Barbanera, S. Berardi, M. Schivalocchi: \u201cClassical\u201d programming-with-proofsin lambda-sym: an analysis of a non-confluence. Proc. TACS\u201997."},{"key":"36_CR3","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/0304-3975(87)90109-5","volume":"52","author":"M. Felleisen","year":"1987","unstructured":"M. Felleisen, D.P. Friedman, E. Kohlbecker, B. Duba: A syntactic theory of sequentialcontrol. Theoretical Computer Science 52(1987) 205\u2013237.","journal-title":"Theoretical Computer Science"},{"key":"36_CR4","first-page":"235","volume":"102","author":"M. Felleisen","year":"1994","unstructured":"M. Felleisen, R. Hieb: The revised report on the syntactic theory of sequentialcontrol and state. Theoretical Computer Science 102 (1994) 235\u2013271.","journal-title":"Theoretical Computer Science"},{"key":"36_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"J.Y. Girard: Linear logic. Theoretical Computer Science. 50 (1987) 1\u2013102.","journal-title":"Theoretical Computer Science"},{"key":"36_CR6","unstructured":"J.Y. Girard, Y. Lafont, and P. Taylor: Proofs and Types. Cambridge UniversityPress, 1989."},{"key":"36_CR7","first-page":"47","volume":"90","author":"T. Griffin","year":"1990","unstructured":"T. Griffin: A formulae-as-types notion of control. Proc. POPL\u201990 (1990) 47\u201358.","journal-title":"Proc. POPL\u2019"},{"key":"36_CR8","unstructured":"M. Hofmann, T. Streicher: Continuation models are universal for \u03b1\u03bc-calculus.Proc. LICS\u201997 (1997) 387\u2013397."},{"key":"36_CR9","unstructured":"M. Hofmann, T. Streicher: Completeness of continuation models for \u03b1\u03bc-calculus.Information and Computation (to appear)."},{"key":"36_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/3-540-55460-2_27","volume-title":"Free Deduction: an Analysis of \u201cComputations\u201d in Classical Logic","author":"M. Parigot","year":"1992","unstructured":"M. Parigot: Free Deduction: an Analysis of \u201cComputations\u201d in Classical Logic.Proc. Russian Conference on Logic Programming, 1991, Springer LNCS 592 361\u2013380."},{"key":"36_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"\u03b1\u03bc-calculus: an Algorithmic Interpretation of Classical Natural Deduction","author":"M. Parigot","year":"1992","unstructured":"M. Parigot: \u03b1\u03bc-calculus: an Algorithmic Interpretation of Classical Natural Deduction.Proc. LPAR\u201992, Springer LNCS 624 (1992) 190\u2013201."},{"key":"36_CR12","doi-asserted-by":"crossref","unstructured":"M. Parigot: Strong normalization for second order classical natural deduction,Proc. LICS\u201993 (1993) 39\u201346.","DOI":"10.1109\/LICS.1993.287602"},{"key":"36_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/3-540-44622-2_32","volume-title":"On the computational interpretation of negation","author":"M. Parigot","year":"2000","unstructured":"M. Parigot: On the computational interpretation of negation, Proc. CSL\u20192000,Springer LNCS 1862 (2000) 472\u2013484."},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"C.H.L. Ong, C.A. Stewart: A Curry-Howard foundation for functional computationwith control. Proc. POPL\u201997 (1997)","DOI":"10.1145\/263699.263722"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"P. Selinger: Control categories and duality: on the categorical semantics of lambdamucalculus, Mathematical Structures in Computer Science (to appear).","DOI":"10.1017\/S096012950000311X"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44450-5_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:16:37Z","timestamp":1556770597000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44450-5_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414131","9783540444503"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-44450-5_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}