{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T19:12:51Z","timestamp":1725995571698},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319479576"},{"type":"electronic","value":"9783319479583"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-47958-3_1","type":"book-chapter","created":{"date-parts":[[2016,10,8]],"date-time":"2016-10-08T13:40:52Z","timestamp":1475934052000},"page":"3-22","source":"Crossref","is-referenced-by-count":2,"title":["Substructural Proofs as Automata"],"prefix":"10.1007","author":[{"given":"Henry","family":"DeYoung","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,9]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic 13(1) (2012)","DOI":"10.1145\/2071368.2071370"},{"key":"1_CR2","unstructured":"Baelde, D., Doumane, A., Saurin, A.: Infinitary proof theory: the multiplicative additive case. In: 25th Conference on Computer Science Logic. LIPIcs, vol. 62, pp. 42:1\u201342:17 (2016)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-642-15375-4_16","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Caires","year":"2010","unstructured":"Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 222\u2013236. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15375-4_16"},{"issue":"3","key":"1_CR4","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1090\/S0002-9947-1936-1501858-0","volume":"39","author":"A Church","year":"1936","unstructured":"Church, A., Rosser, J.: Some properties of conversion. Trans. Am. Math. Soc. 39(3), 472\u2013482 (1936)","journal-title":"Trans. Am. Math. Soc."},{"key":"1_CR5","doi-asserted-by":"crossref","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"HB Curry","year":"1934","unstructured":"Curry, H.B.: Functionality in combinatory logic. Proc. Nat. Acad. Sci. U.S.A. 20, 584\u2013590 (1934)","journal-title":"Proc. Nat. Acad. Sci. U.S.A."},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-28869-2_10","volume-title":"Programming Languages and Systems","author":"P-M Deni\u00e9lou","year":"2012","unstructured":"Deni\u00e9lou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 194\u2013213. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28869-2_10"},{"key":"1_CR7","unstructured":"DeYoung, H., Caires, L., Pfenning, F., Toninho, B.: Cut reduction in linear logic as asynchronous session-typed communication. In: 21st Conference on Computer Science Logic. LIPIcs, vol. 16, pp. 228\u2013242 (2012)"},{"key":"1_CR8","volume-title":"The Logical Basis of Metaphysics","author":"M Dummett","year":"1991","unstructured":"Dummett, M.: The Logical Basis of Metaphysics. Harvard University Press, Cambridge (1991). From the William James Lectures 1976"},{"key":"1_CR9","unstructured":"Fortier, J., Santocanale, L.: Cuts for circular proofs: semantics and cut elimination. In: 22nd Conference on Computer Science Logic. LIPIcs, vol. 23, pp. 248\u2013262 (2013)"},{"issue":"2","key":"1_CR10","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","volume":"42","author":"S Gay","year":"2005","unstructured":"Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2), 191\u2013225 (2005)","journal-title":"Acta Informatica"},{"issue":"1","key":"1_CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"JY Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50(1), 1\u2013102 (1987)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR12","unstructured":"Howard, W.A.: The formulae-as-types notion of construction (1969), unpublished note. An annotated version appeared in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490, Academic Press (1980)"},{"issue":"1","key":"1_CR13","first-page":"11","volume":"1","author":"P Martin-L\u00f6f","year":"1996","unstructured":"Martin-L\u00f6f, P.: On the meanings of the logical constants and the justifications of the logical laws. Nord. J. Philos. Logic 1(1), 11\u201360 (1996)","journal-title":"Nord. J. Philos. Logic"},{"issue":"2","key":"1_CR14","first-page":"269","volume":"23","author":"M Mohri","year":"1997","unstructured":"Mohri, M.: Finite-state transducers in language and speech processing. J. Comput. Linguist. 23(2), 269\u2013311 (1997)","journal-title":"J. Comput. Linguist."},{"issue":"1","key":"1_CR15","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0304-3975(77)90055-X","volume":"4","author":"MP Sch\u00fctzenberger","year":"1977","unstructured":"Sch\u00fctzenberger, M.P.: Sur une variante des fonctions sequentielles. Theoret. Comput. Sci. 4(1), 47\u201357 (1977)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"1_CR16","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"AM Turing","year":"1937","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. Lond. Math. Soc. 42(2), 230\u2013265 (1937)","journal-title":"Proc. Lond. Math. Soc."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47958-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,25]],"date-time":"2017-06-25T00:40:32Z","timestamp":1498351232000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47958-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319479576","9783319479583"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47958-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}