{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:07:54Z","timestamp":1760202474690,"version":"3.43.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1997,11,1]],"date-time":"1997-11-01T00:00:00Z","timestamp":878342400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,11,1]],"date-time":"1997-11-01T00:00:00Z","timestamp":878342400000},"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":["Studia Logica"],"published-print":{"date-parts":[[1997,11]]},"DOI":"10.1023\/a:1005092630115","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T15:31:12Z","timestamp":1040484672000},"page":"417-448","source":"Crossref","is-referenced-by-count":9,"title":["Lambda Calculus and Intuitionistic Linear Logic"],"prefix":"10.1007","volume":"59","author":[{"given":"Simona Ronchi","family":"della Rocca","sequence":"first","affiliation":[]},{"given":"Luca","family":"Roversi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"149767_CR1","series-title":"Technical Report","volume-title":"Computational interpretation of linear logic","author":"S. Abramsky","year":"1990","unstructured":"S. Abramsky, 1990, Computational interpretation of linear logic, Technical Report 90\/92, Department of Computing, Imperial College, London."},{"key":"149767_CR2","series-title":"Technical Report","volume-title":"Games and full completeness for multiplicative linear logic","author":"S. Abramsky","year":"1992","unstructured":"S. Abramsky and R. Jagadeesan, 1992, Games and full completeness for multiplicative linear logic, Technical Report 92\/24, Department of Computing, Imperial College, London, September."},{"unstructured":"H.P. Barendregt, 1984, The Lambda Calculus, North-Holland, second edition.","key":"149767_CR3"},{"unstructured":"N. Benton, G. Bierman, V. de Paiva, and M. Hyland, 1990, Term assignment for intuitionistic linear logic. Technical Report 262, Computer Laboratory, University of Cambridge, August.","key":"149767_CR4"},{"doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen, D. Kesner, and L. Puel, 1993, A typed pattern calculus, In Proceedings of the 8th Symposium on Logic in Computer Science LICS'93 (Montreal), pages 262\u2013274, June.","key":"149767_CR5","DOI":"10.1109\/LICS.1993.287581"},{"unstructured":"J. Gallier, 1990, Logic and Computer Science, chapter On Girard's \u201ccandidats de reductibilit\u00e9s\u201d, pages 123\u2013203, P. Odifreddi editor, Academic Press.","key":"149767_CR6"},{"unstructured":"J. Gallier, 1993, On the correspondence between proofs and lambda terms, Obtained by ftp, January.","key":"149767_CR7"},{"unstructured":"J.Y. Girard, 1972, Interpretation Fonctionelle et Elimination des Coupures de l'Arithmetique d'Ordre Superieur, PhD thesis, Universit\u00e9 Paris VII.","key":"149767_CR8"},{"key":"149767_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"J.Y. Girard, 1987, Linear logic Theoretical Computer Science, 50:1\u2013102.","journal-title":"Theoretical Computer Science"},{"unstructured":"J.Y. Girard, Y. Lafont, and P. Taylor, 1989, Proofs and Types, Cambridge University Press.","key":"149767_CR10"},{"key":"149767_CR11","first-page":"797","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet, 1980, Confluent reductions: abstract properties and applications to term rewriting systems, Journal of A.C.M., 27:797\u2013821.","journal-title":"Journal of A.C.M."},{"unstructured":"B. Jacobs, 1992, Semantics of weakening and contraction, In Typed Lambda Calculi and Applications TLCA'92, volume LNGS. Springer-Verlag.","key":"149767_CR12"},{"key":"149767_CR13","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(88)90100-4","volume":"59","author":"Y. Lafont","year":"1988","unstructured":"Y. Lafont, 1988, The linear abstract machine, Theoretical Computer Science, 59:157\u2013180.","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"P. Lincoln and J. Mitchell, 1992, Operational aspects of linear lambda calculus, In Proceedings of Symposium on Logic in Computer Science LICS'92, pages 235\u2013246, June.","key":"149767_CR14","DOI":"10.1109\/LICS.1992.185536"},{"doi-asserted-by":"crossref","unstructured":"Simone Martini and Andrea Masini, 1993, On the fine structure of the exponential rule. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 197\u2013210. Cambridge University Press, 1995. Proceedings of the Workshop on Linear Logic, Ithaca, New York, June.","key":"149767_CR15","DOI":"10.1017\/CBO9780511629150.010"},{"unstructured":"G. Mints, Normal deductions in the intuitionistic linear logic. To appear in Archive for Mathematical Logic.","key":"149767_CR16"},{"unstructured":"A. Pravato and L. Roversi, 1995, A! considered both as a paradigmatic language and as a meta-language, In Theoretical Computer Science: Proceedings of the Fifth Italian Conference (Salerno), pages 146\u2013161. World Scientific, November.","key":"149767_CR17"},{"key":"149767_CR18","volume-title":"Natural Deduction, a Proof Theoretic Study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz, 1965. Natural Deduction, a Proof Theoretic Study, Almquist and Wiksell-Amsterdam."},{"doi-asserted-by":"crossref","unstructured":"J.A. Reynolds, 1974, Paris Colloquium on Programming, chapter Towards a Theory of Type Structures, pages 408\u2013425. Springer-Verlag.","key":"149767_CR19","DOI":"10.1007\/3-540-06859-7_148"},{"unstructured":"S. Ronchi della Rocca and L. Roversi 1994, Lambda calculus and intuitionistic linear logic, Invited talk at the Logic Colloquium'94 (Clermont-Ferrand), July.","key":"149767_CR20"},{"unstructured":"L. Roversi, 1996, Curry-Howard isomorphism and intuitionistic linear logic, Technical Report 19\/96, Universit\u00e0 degli Studi di Torino.","key":"149767_CR21"},{"doi-asserted-by":"crossref","unstructured":"A.S. Troelstra, 1992, Lectures on Linear Logic, CSLI.","key":"149767_CR22","DOI":"10.1093\/oso\/9780198537779.003.0013"},{"doi-asserted-by":"crossref","unstructured":"P. Wadler, 1993 A syntax for linear logic, Presented at the Mathematical Foundations of Programming Semantics, New Orleans, April.","key":"149767_CR23","DOI":"10.1007\/3-540-58027-1_24"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005092630115.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005092630115\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005092630115.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:11:20Z","timestamp":1754629880000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005092630115"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,11]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,11]]}},"alternative-id":["149767"],"URL":"https:\/\/doi.org\/10.1023\/a:1005092630115","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[1997,11]]}}}