{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:21:52Z","timestamp":1755220912183,"version":"3.43.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2002,8,1]],"date-time":"2002-08-01T00:00:00Z","timestamp":1028160000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,8,1]],"date-time":"2002-08-01T00:00:00Z","timestamp":1028160000000},"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":[[2002,8]]},"DOI":"10.1023\/a:1020568830946","type":"journal-article","created":{"date-parts":[[2003,3,18]],"date-time":"2003-03-18T15:12:43Z","timestamp":1048000363000},"page":"331-353","source":"Crossref","is-referenced-by-count":7,"title":["Bicartesian Coherence"],"prefix":"10.1007","volume":"71","author":[{"given":"Kosta","family":"Do\u0161en","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zoran","family":"Petri\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5098764_CR1","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1017\/S0960129500000232","volume":"3","author":"J. R. B. Cockett","year":"1993","unstructured":"Cockett, J. R. B., \u2018Introduction to distributive categories\u2019, Mathematical Structures in Computer Science 3 (1993), 277-307.","journal-title":"Mathematical Structures in Computer Science"},{"key":"5098764_CR2","first-page":"63","volume":"8","author":"J. R. B. Cockett","year":"2001","unstructured":"Cockett, J. R. B., and R. A. G. Seely, \u2018Finite sum-product logic\u2019, Theory and Application of Categories 8 (2001), 63-99 (preliminary draft, March 2000).","journal-title":"Theory and Application of Categories"},{"key":"5098764_CR3","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1002\/1521-3870(200101)47:1<137::AID-MALQ137>3.0.CO;2-F","volume":"47","author":"K. Do\u0160en","year":"2001","unstructured":"Do\u0160en, K., and Z. Petri\u0106, \u2018The maximality of cartesian categories\u2019, Mathematical Logic Quarterly 47 (2001), 137-144 (available at: http:\/\/xxx.lanl.gov\/math.CT\/9911059).","journal-title":"Mathematical Logic Quarterly"},{"issue":"82","key":"5098764_CR4","first-page":"1","volume":"68","author":"K. Do\u0160en","year":"2000","unstructured":"Do\u0160en, K., and Z. Petri\u0106, \u2018The maximality of the typed lambda calculus and of cartesian closed categories\u2019, Publications de l'Institut Math\u00e9matique (N.S.) 68(82) (2000), 1-19 (available at: http:\/\/xxx.lanl.gov\/math.CT\/9911073).","journal-title":"Publications de l'Institut Math\u00e9matique (N.S.)"},{"key":"5098764_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/3-540-45504-3_6","volume-title":"Proof Theory in Computer Science","author":"K. Do\u0160en","year":"2001","unstructured":"Do\u0160en, K., and Z. Petri\u0106, \u2018Coherent bicartesian and sesquicartesian categories\u2019, R. Kahle et al. (eds.), Proof Theory in Computer Science, Lecture Notes in Computer Science 2183, Springer, Berlin, 2001, pp. 78-92 (available at: http:\/\/xxx.lanl.gov\/math.CT\/0006091)."},{"key":"5098764_CR6","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/BF01451367","volume":"145","author":"B. Eckmann","year":"1962","unstructured":"Eckmann, B., and P. J. Hilton, \u2018Group-like structures in general categories I: Multiplication and comultiplication\u2019, Mathematische Annalen 145 (1962), 227-255.","journal-title":"Mathematische Annalen"},{"key":"5098764_CR7","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1016\/0021-8693(66)90006-8","volume":"3","author":"S. Eilenberg","year":"1966","unstructured":"Eilenberg, S., and G. M. Kelly, \u2018A generalization of the functorial calculus\u2019, Journal of Algebra 3 (1966), 366-375.","journal-title":"Journal of Algebra"},{"key":"5098764_CR8","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0022-4049(71)90013-2","volume":"1","author":"G. M. Kelly","year":"1971","unstructured":"Kelly, G. M., and S. Mac Lane, \u2018Coherence in closed categories\u2019, Journal of Pure and Applied Algebra 1 (1971), 97-140, 219.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"5098764_CR9","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/BFb0059557","volume-title":"Coherence in Categories","author":"G. M. Kelly","year":"1972","unstructured":"Kelly, G. M., \u2018An abstract approach to coherence\u2019, in [16], pp. 106-147."},{"key":"5098764_CR10","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF01703261","volume":"2","author":"J. Lambek","year":"1968","unstructured":"Lambek, J., \u2018Deductive systems and categories I: Syntactic calculus and residuated categories\u2019, Mathematical Systems Theory 2 (1968), 287-318.","journal-title":"Mathematical Systems Theory"},{"key":"5098764_CR11","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/BFb0079385","volume-title":"Category Theory, Homology Theory and their Applications I","author":"J. Lambek","year":"1969","unstructured":"Lambek, J., \u2018Deductive systems and categories II: Standard constructions and closed categories\u2019, in Category Theory, Homology Theory and their Applications I, Lecture Notes in Mathematics 86, Springer, Berlin 1969, pp. 76-122."},{"key":"5098764_CR12","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BFb0073965","volume-title":"Toposes, Algebraic Geometry and Logic","author":"J. Lambek","year":"1972","unstructured":"Lambek, J., \u2018Deductive systems and categories III: Cartesian closed categories, intuitionist propositional calculus, and combinatory logic\u2019, in F. W. Lawvere (ed.), Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, Springer, Berlin 1972, pp. 57-82."},{"key":"5098764_CR13","volume-title":"Introduction to Higher-Order Categorical Logic","author":"J. Lambek","year":"1986","unstructured":"Lambek, J., and P. J. Scott, Introduction to Higher-Order Categorical Logic, Cambridge University Press, Cambridge 1986."},{"key":"5098764_CR14","volume-title":"Conceptual Mathematics: A First Introduction to Categories","author":"F. W. Lambek","year":"1997","unstructured":"Lambek, F. W., and S. H. Schanuel, Conceptual Mathematics: A First Introduction to Categories, Cambridge University Press, Cambridge 1997 (first edition: Buffalo Workshop Press, Buffalo 1991)."},{"key":"5098764_CR15","first-page":"28","volume":"49","author":"S. Mac Lane","year":"1963","unstructured":"Mac Lane, S., \u2018Natural associativity and commutativity\u2019, Rice University Studies, Papers in Mathematics 49 (1963), 28-46.","journal-title":"Rice University Studies, Papers in Mathematics"},{"key":"5098764_CR16","series-title":"Lecture Notes in Mathematics","volume-title":"Coherence in Categories","year":"1972","unstructured":"Mac Lane, S., (ed.), Coherence in Categories, Lecture Notes in Mathematics 281, Springer, Berlin 1972."},{"key":"5098764_CR17","first-page":"252","volume-title":"Aktual'nye voprosy logiki i metodologii nauki","author":"G. E. Mints","year":"1980","unstructured":"Mints, G. E., \u2018Category theory and proof theory (in Russian)\u2019, in Aktual'nye voprosy logiki i metodologii nauki, Naukova Dumka, Kiev 1980, pp. 252-278 (English translation, with permuted title, in G. E. Mints, Selected Papers in Proof Theory, Bibliopolis, Naples 1992)."},{"key":"5098764_CR18","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1023\/A:1015186718090","volume":"70","author":"Z. Petri\u0106","year":"2002","unstructured":"Petri\u0106, Z., \u2018Coherence in substructural categories\u2019, Studia Logica 70 (2002), 271-296.","journal-title":"Studia Logica"},{"key":"5098764_CR19","doi-asserted-by":"crossref","first-page":"319","DOI":"10.3233\/FI-1993-182-417","volume":"18","author":"J. Rebagliato","year":"1993","unstructured":"Rebagliato, J., and V. Verd\u00da, \u2018On the algebraization of some Gentzen systems\u2019, Fundamenta Informaticae 18 (1993), 319-338.","journal-title":"Fundamenta Informaticae"},{"key":"5098764_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/BFb0014068","volume-title":"Typed Lambda Calculi and Applications (Edinburgh, 1995)","author":"A. K. Simpson","year":"1995","unstructured":"Simpson, A. K., \u2018Categorical completeness results for the simply-typed lambdacalculus\u2019, in M. Dezani-Ciancaglini and G. Plotkin (eds.), Typed Lambda Calculi and Applications (Edinburgh, 1995), Lecture Notes in Computer Science 902, Springer, Berlin 1995, pp. 414-427."},{"key":"5098764_CR21","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1305\/ndjfl\/1093891297","volume":"15","author":"M. E. Szabo","year":"1974","unstructured":"Szabo, M. E., \u2018A categorical equivalence of proofs\u2019, Notre Dame Journal of Formal Logic 15 (1974), 177-191.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"5098764_CR22","doi-asserted-by":"crossref","first-page":"111","DOI":"10.4153\/CMB-1975-020-1","volume":"18","author":"M. E. Szabo","year":"1975","unstructured":"Szabo, M. E., \u2018A counter-example to coherence in cartesian closed categories\u2019, Canadian Mathematical Bulletin 18 (1975), 111-114.","journal-title":"Canadian Mathematical Bulletin"},{"key":"5098764_CR23","volume-title":"Algebra of Proofs","author":"M. E. Szabo","year":"1978","unstructured":"Szabo, M. E., Algebra of Proofs, North-Holland, Amsterdam 1978."},{"key":"5098764_CR24","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00370826","volume":"48","author":"M. E. Szabo","year":"1989","unstructured":"Szabo, M. E., \u2018Coherence in cartesian closed categories and the generality of proofs\u2019, Studia Logica 48 (1989), 285-297.","journal-title":"Studia Logica"},{"key":"5098764_CR25","volume-title":"Basic Proof Theory","author":"A. S. Troelstra","year":"1996","unstructured":"Troelstra, A. S., and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, Cambridge 1996."},{"key":"5098764_CR26","doi-asserted-by":"crossref","first-page":"331","DOI":"10.2307\/421184","volume":"5","author":"R. Zach","year":"1999","unstructured":"Zach, R., \u2018Completeness before Post: Bernays, Hilbert and the development of propositional logic\u2019, The Bulletin of Symbolic Logic 5 (1999), 331-366.","journal-title":"The Bulletin of Symbolic Logic"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020568830946.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1020568830946\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020568830946.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:24:17Z","timestamp":1754630657000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1020568830946"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,8]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2002,8]]}},"alternative-id":["5098764"],"URL":"https:\/\/doi.org\/10.1023\/a:1020568830946","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2002,8]]}}}