{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:21:53Z","timestamp":1755220913628,"version":"3.43.0"},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,9,1]],"date-time":"1998-09-01T00:00:00Z","timestamp":904608000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,9,1]],"date-time":"1998-09-01T00:00:00Z","timestamp":904608000000},"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":[[1998,9]]},"DOI":"10.1023\/a:1005025414656","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T15:31:12Z","timestamp":1040484672000},"page":"223-235","source":"Crossref","is-referenced-by-count":0,"title":["Curry-Howard Terms for Linear Logic"],"prefix":"10.1007","volume":"61","author":[{"given":"Frank A.","family":"B\u00e4uerle","sequence":"first","affiliation":[]},{"given":"David","family":"Albrecht","sequence":"additional","affiliation":[]},{"given":"John N.","family":"Crossley","sequence":"additional","affiliation":[]},{"given":"John S.","family":"Jeavons","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"184246_CR1","series-title":"Springer Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/BFb0037099","volume-title":"Typed Larnbda Calculi and Applications, International Conference TLCA '93","author":"N. Benton","year":"1993","unstructured":"Benton, N., G. Bierman, V. de Paiva and M. Hyland, \u2018A Term Calculus for Intuitionistic Linear Logic\u2019, p. 75\u201390 in Typed Larnbda Calculi and Applications, International Conference TLCA '93, Springer Lecture Notes in Computer Science 664, Springer, Berlin (1993)."},{"key":"184246_CR2","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-1-4612-0325-4_8","volume-title":"Logical Methods","author":"J. N. Crossley","year":"1993","unstructured":"Crossley, J. N., and J. C. Shepherdson, \u2018Extracting programs from proofs by an extension of the Curry-Howard process\u2019, p. 222\u2013288 in Logical Methods, ed. J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler, Birkh\u00e4user, Boston (1993)."},{"key":"184246_CR3","volume-title":"The Collected Papers of Gerhard Gentzen","author":"M. E. Szabo","year":"1969","unstructured":"Szabo, M. E., The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam (1969)."},{"key":"184246_CR4","unstructured":"Girard, J.-Y., Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e9se de Doctorat d'\u00c9tat, Universit\u00e9 Paris VII (1972)."},{"key":"184246_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y., \u2018Linear logic\u2019, Theoretical Computer Science 50 (1987), 1\u2013102.","journal-title":"Theoretical Computer Science"},{"key":"184246_CR6","unstructured":"Girard, J.-Y., \u2018Linear logic: a survey\u2019, preprint Laboratoire de Math\u00e9matiques Discr\u00e9tes."},{"key":"184246_CR7","volume-title":"Feasible mathematics","author":"J.-Y. Girard","year":"1990","unstructured":"Girard, J.-Y., A. Scedrov and P. J. Scott, \u2018Bounded linear logic: a modular approach to polynomial time computability\u2019, extended abstract in Feasible mathematics, eds. Buss & P. J. Scott, Birkh\u00e4user, Boston, 1990; complete version in TCS 97 (1992), 1\u201366."},{"key":"184246_CR8","first-page":"479","volume-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W. A. Howard","year":"1980","unstructured":"Howard, W. A., \u2018The formulae-as-types notion of construction\u2019, p. 479\u2013490 in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, eds. J. P. Soldin and J. R. Hindley, Academic Press, London (1980)."},{"key":"184246_CR9","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"Tait, W. W., \u2018Intensional interpretation of functionals of finite type I\u2019, Journal of Symbolic Logic 32 (1967), 198\u2013212.","journal-title":"Journal of Symbolic Logic"},{"key":"184246_CR10","volume-title":"Lectures on Linear Logic","author":"A. S. Troelstra","year":"1992","unstructured":"Troelstra, A. S., Lectures on Linear Logic, Stanford, CA: Center for the study of language and information, Nr. 29, 1992."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005025414656.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005025414656\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005025414656.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:13:33Z","timestamp":1754630013000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005025414656"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,9]]},"references-count":10,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,9]]}},"alternative-id":["184246"],"URL":"https:\/\/doi.org\/10.1023\/a:1005025414656","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[1998,9]]}}}