{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T14:11:48Z","timestamp":1770732708190,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_34","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"392-407","source":"Crossref","is-referenced-by-count":9,"title":["Automating Proofs in Category Theory"],"prefix":"10.1007","author":[{"given":"Dexter","family":"Kozen","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Kreitz","sequence":"additional","affiliation":[]},{"given":"Eva","family":"Richter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","doi-asserted-by":"crossref","unstructured":"Allen, S., et al.: Innovations in computational type theory using Nuprl. Journal of Applied Logic (to appear, 2006)","DOI":"10.1016\/j.jal.2005.10.005"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/10721959_12","volume-title":"Automated Deduction - CADE-17","author":"S. Allen","year":"2000","unstructured":"Allen, S., Constable, R., Eaton, R., Kreitz, C., Lorigo, L.: The Nuprl open logical environment. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 170\u2013176. Springer, Heidelberg (2000)"},{"key":"34_CR3","unstructured":"Bancerek, G.: Concrete categories. J.\u00a0formalized mathematics\u00a013 (2001)"},{"key":"34_CR4","unstructured":"Bancerek, G.: Miscellaneous facts about functors. J.\u00a0form.\u00a0math. 13 (2001)"},{"key":"34_CR5","unstructured":"Bancerek, G.: Categorial background for duality theory. J. form. math. 13 (2001)"},{"key":"34_CR6","volume-title":"Category Theory for Computing Science","author":"M. Barr","year":"1990","unstructured":"Barr, M., Wells, C.: Category Theory for Computing Science. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"34_CR7","first-page":"287","volume-title":"A Calculus of Functions for Program Derivation, Research Topics in Functional Programming","author":"R. Bird","year":"1990","unstructured":"Bird, R.: A Calculus of Functions for Program Derivation, Research Topics in Functional Programming, pp. 287\u2013307. Addison-Wesley, Reading (1990)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"Bundy, A.: The Use of Explicit Plans to Guide Inductive Proofs. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 111\u2013120. Springer, Heidelberg (1988)"},{"key":"34_CR9","volume-title":"Implementing Mathematics with the Nuprl proof development system","author":"R. Constable","year":"1986","unstructured":"Constable, R., et al.: Implementing Mathematics with the Nuprl proof development system. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"C\u00e1ccamo, M.J., Winskel, G.: A higher-order calculus for categories. Technical Report RS-01-27, BRICS, University of Aarhus (2001)","DOI":"10.7146\/brics.v8i27.21687"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Eklund, P., et al.: A graphical approach to monad compositions. Electronic Notes in Theoretical Computer Science 40 (2002)","DOI":"10.1016\/S1571-0661(05)80041-6"},{"key":"34_CR12","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1090\/S0002-9947-1945-0013131-6","volume":"58","author":"S. Eilenberg","year":"1945","unstructured":"Eilenberg, S., MacLane, S.: General theory of natural equivalences. Trans. Amer. Math. Soc.\u00a058, 231\u2013244 (1945)","journal-title":"Trans. Amer. Math. Soc."},{"key":"34_CR13","unstructured":"Glimming, J.: Logic and automation for algebra of programming. Master thesis, University of Oxford (2001)"},{"issue":"1","key":"34_CR14","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1017\/S0960129500000050","volume":"1","author":"J. Goguen","year":"1991","unstructured":"Goguen, J.: A categorical manifesto. Mathematical Structures in Computer Science\u00a01(1), 49\u201367 (1991)","journal-title":"Mathematical Structures in Computer Science"},{"key":"34_CR15","unstructured":"Harrison, J.: Formalized mathematics. Technical report of Turku Centre for Computer Science 36 (1996)"},{"key":"34_CR16","volume-title":"Joint CLICS-TYPES Workshop on Categories and Type Theory","author":"G. Huet","year":"1995","unstructured":"Huet, G., Sa\u00efbi, A.: Constructive category theory. In: Joint CLICS-TYPES Workshop on Categories and Type Theory, MIT Press, Cambridge (1995)"},{"key":"34_CR17","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebra. In: Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"34_CR18","unstructured":"Kozen, D.: Toward the automation of category theory. Technical Report 2004-1964, Computer Science Department, Cornell University (2004)"},{"key":"34_CR19","unstructured":"Kreitz, C.: The Nuprl Proof Development System, V5: Reference Manual and User\u2019s Guide. Computer Science Department, Cornell University (2002)"},{"key":"34_CR20","volume-title":"Categories for the Working Mathematician","author":"S. MacLane","year":"1971","unstructured":"MacLane, S.: Categories for the Working Mathematician. Springer, Heidelberg (1971)"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Notions of computation and monads. Inf. and Comp.\u00a093 (1991)","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"34_CR22","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"212","volume-title":"Towards a readable formalisation of category theory","author":"G. O\u2019Keefe","year":"2004","unstructured":"O\u2019Keefe, G.: Towards a readable formalisation of category theory. Electronic Notes in Theoretical Computer Science, vol.\u00a091, pp. 212\u2013228. Elsevier, Amsterdam (2004)"},{"key":"34_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"34_CR24","volume-title":"Computational Category Theory","author":"D. Rydeheard","year":"1988","unstructured":"Rydeheard, D., Burstall, R.: Computational Category Theory. Prentice-Hall, Englewood Cliffs (1988)"},{"key":"34_CR25","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537601.001.0001","volume-title":"Topology and Category Theory in Computer Science","author":"G.M. Reed","year":"1991","unstructured":"Reed, G.M., Roscoe, A.W., Wachter, R.F.: Topology and Category Theory in Computer Science. Oxford University Press, Oxford (1991)"},{"key":"34_CR26","unstructured":"Sa\u00efbi, A.: Constructive category theory (1995), http:\/\/coq.inria.fr\/contribs\/category.tar.gz"},{"key":"34_CR27","unstructured":"Simpson, C.: Category theory in ZFC (2004), coq.inria.fr\/contribs\/CatsInZFC.tar.gz"},{"key":"34_CR28","unstructured":"Takeyama, M.: Universal Structure and a Categorical Framework for Type Theory. PhD thesis, University of Edinburgh (1995)"},{"key":"34_CR29","unstructured":"Trybulec, A.: Some isomorphisms between functor categories. J.\u00a0formalized mathematics 4 (1992)"},{"key":"34_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P. Wadler","year":"1995","unstructured":"Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol.\u00a0925, pp. 24\u201352. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,7]],"date-time":"2024-02-07T00:48:28Z","timestamp":1707266908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11814771_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}