{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,28]],"date-time":"2025-12-28T02:17:53Z","timestamp":1766888273186},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433668"},{"type":"electronic","value":"9783540459316"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45931-6_25","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T00:53:52Z","timestamp":1181350432000},"page":"357-371","source":"Crossref","is-referenced-by-count":30,"title":["A Calculus of Circular Proofs and Its Categorical Semantics"],"prefix":"10.1007","author":[{"given":"Luigi","family":"Santocanale","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,3,15]]},"reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"publisher","first-page":"543","DOI":"10.2307\/2275407","volume":"59","author":"S. Abramsky","year":"1994","unstructured":"S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symbolic Logic, 59(2):543\u2013574, 1994.","journal-title":"J. Symbolic Logic"},{"key":"25_CR2","unstructured":"P. Aczel. Non-well-founded sets. Stanford University Center for the Study of Language and Information, Stanford, CA, 1988."},{"key":"25_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511600579","volume-title":"Locally presentable and accessible categories","author":"J. Ad\u00e1mek","year":"1994","unstructured":"J. Ad\u00e1mek and J. Rosick\u00ed. Locally presentable and accessible categories. Cam bridge University Press, Cambridge, 1994."},{"key":"25_CR4","unstructured":"A. Arnold and D. Niwinski. Rudiments of mu-calculus. Number 146 in Studies in Logic and the Foundations of Mathematics. Elsevier (North-Holland), 2001."},{"issue":"1\u20133","key":"25_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0168-0072(92)90073-9","volume":"56","author":"A. Blass","year":"1992","unstructured":"A. Blass. A game semantics for linear logic. Ann. Pure Appl. Logic, 56(1\u20133):183\u2013220, 1992.","journal-title":"Ann. Pure Appl. Logic"},{"key":"25_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-78034-9","volume-title":"Iteration theories","author":"S. L. Bloom","year":"1993","unstructured":"S. L. Bloom and Z. \u00c9sik. Iteration theories. Springer-Verlag, Berlin, 1993.The equational logic of iterative processes."},{"issue":"2","key":"25_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1023\/A:1008708924144","volume":"9","author":"S. L. Bloom","year":"2001","unstructured":"S. L. Bloom, Z. \u00c9sik, A. Labella, and E. G. Manes. Iteration 2-theories. Appl. Categ. Structures, 9(2):173\u2013216, 2001.","journal-title":"Appl. Categ. Structures"},{"key":"25_CR8","first-page":"63","volume":"8","author":"J. R. B. Cockett","year":"2001","unstructured":"J. R. B. Cockett and R. A. G. Seely. Finite sum-product logic. Theory and Applications of Categories, 8:63\u201399, 2001.","journal-title":"Theory and Applications of Categories"},{"key":"25_CR9","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-58085-9_72","volume-title":"Types for proofs and programs (Nijmegen, 1993)","author":"T. Coquand","year":"1994","unstructured":"T. Coquand. Infinite objects in type theory. In Types for proofs and programs (Nijmegen, 1993), pages 62\u201378.Springer, Berlin, 1994."},{"key":"25_CR10","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88 (Tallinn, 1988)","author":"T. Coquand","year":"1990","unstructured":"T. Coquand and C. Paulin. Inductively defined types. In COLOG-88 (Tallinn, 1988), pages 50\u201366. Springer, Berlin, 1990."},{"issue":"1","key":"25_CR11","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear logic. Theoret. Comput. Sci., 50(1):101, 1987.","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"25_CR12","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0304-3975(99)00051-1","volume":"227","author":"H. Hu","year":"1999","unstructured":"H. Hu and A. Joyal. Coherence completions of categories. Theoret. Comput. Sci., 227(1\u20132):153\u2013184, 1999. Linear logic, I (Tokyo, 1996).","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"25_CR13","doi-asserted-by":"publisher","first-page":"451","DOI":"10.2307\/2586843","volume":"63","author":"A. J. C. Hurkens","year":"1998","unstructured":"A. J. C. Hurkens, M. McArthur, Y. N. Moschovakis, L. S. Moss, and G. T. Whitney. The logic of recursive equations. J. Symbolic Logic, 63(2):451\u2013478, 1998.","journal-title":"J. Symbolic Logic"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"A. Joyal. Free lattices, communication, and money games. In Logic and scientific methods, pages 29\u201368. Kluwer Academic Publishers, 1997.","DOI":"10.1007\/978-94-017-0487-8_3"},{"issue":"3","key":"25_CR15","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the propositional \u03bc-calculus. Theoret. Comput. Sci., 27(3):333\u2013354, 1983.","journal-title":"Theoret. Comput. Sci."},{"key":"25_CR16","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF01110627","volume":"103","author":"J. Lambek","year":"1968","unstructured":"J. Lambek. A fixpoint theorem for complete categories. Math. Z., 103:151\u2013161, 1968.","journal-title":"Math. Z."},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-49019-1_17","volume-title":"Foundations of software science and computation structures (Amsterdam, 1999)","author":"M. Lenisa","year":"1999","unstructured":"M. Lenisa. A complete coinductive logical system for bisimulation equivalence on circular objects. In Foundations of software science and computation structures (Amsterdam, 1999), pages 243\u2013257. Springer, Berlin, 1999."},{"issue":"1","key":"25_CR18","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J. J. M. M. Rutten","year":"2000","unstructured":"J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3\u201380, 2000.","journal-title":"Theoret. Comput. Sci."},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"L. Santocanale. The alternation hierarchy for the theory of \u03bc-lattices. Technical Report RS-00-29, BRICS, November 2000. To appear in Theory and Applications of Categories.","DOI":"10.7146\/brics.v7i29.20163"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"L. Santocanale. Free \u03bc-lattices. Technical Report RS-00-28, BRICS, November 2000. To appear in Journal of Pure and Applied Algebra.","DOI":"10.7146\/brics.v7i28.20161"},{"key":"25_CR21","unstructured":"L. Santocanale. Sur les \u03bc-treillis libres. PhD thesis, Universit\u00e9 du Qu\u00e9bec \u00e0 Montr\u00e9al, July 2000."},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"L. Santocanale. Acalculus of circular proofs and its categorical semantics. Technical Report RS-01-15, BRICS, May 2001. Extended version available from: http:\/\/www.cpsc.ucalgary.ca\/~luigis\/ .","DOI":"10.7146\/brics.v8i15.20472"},{"key":"25_CR23","unstructured":"L. Santocanale. Parity functors and \u03bc-bicomplete categories (extended abstract). In Fixed Points in Computer Science 2001, September 2001. Extended version submitted."},{"issue":"3","key":"25_CR24","first-page":"343","volume":"6","author":"T. Uustalu","year":"1999","unstructured":"T. Uustalu and V. Vene. Mendler-style inductive types, categorically. Nordic J. Comput., 6(3):343\u2013361, 1999. Programming theory (Turku, 1998).","journal-title":"Nordic J. Comput."},{"issue":"2","key":"25_CR25","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(90)90147-A","volume":"73","author":"P. Wadler","year":"1990","unstructured":"P. Wadler. Deforestation: transforming programs to eliminate trees. Theoret. Comput. Sci., 73(2):231\u2013248, 1990.","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"25_CR26","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1006\/inco.1999.2836","volume":"157","author":"I. Walukiewicz","year":"2000","unstructured":"I. Walukiewicz. Completeness of Kozen\u2019s axiomatisation of the propositional \u03bc-calculus. Inform. and Comput., 157(1\u20132):142\u2013182, 2000. LICS 1995 (San Diego, CA).","journal-title":"Inform. and Comput."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45931-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T19:19:27Z","timestamp":1556479167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45931-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433668","9783540459316"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45931-6_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}