{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:38:33Z","timestamp":1742935113692,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031427527"},{"type":"electronic","value":"9783031427534"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-42753-4_5","type":"book-chapter","created":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T06:02:35Z","timestamp":1693375355000},"page":"69-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Category Theory in\u00a0Isabelle\/HOL as\u00a0a\u00a0Basis for\u00a0Meta-logical Investigation"],"prefix":"10.1007","author":[{"given":"Jonas","family":"Bayer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Gonus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dana S.","family":"Scott","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,8,28]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-12821-9_1","volume-title":"New Structures for Physics","author":"S Abramsky","year":"2011","unstructured":"Abramsky, S., Tzevelekos, N.: Introduction to categories and categorical logic. In: Coecke, B. (ed.) New Structures for Physics, pp. 3\u201394. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-12821-9_1"},{"key":"5_CR2","unstructured":"Beffara, E.: Introduction to linear logic, August 2013. https:\/\/hal.archives-ouvertes.fr\/cel-01144229, lecture"},{"key":"5_CR3","unstructured":"Benzm\u00fcller, C., Andrews, P.: Church\u2019s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Summer 2019 edn., pp. 1\u201362 (in pdf version). Metaphysics Research Lab, Stanford University (2019). https:\/\/plato.stanford.edu\/entries\/type-theory-church\/"},{"key":"5_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103348","volume":"287","author":"C Benzm\u00fcller","year":"2020","unstructured":"Benzm\u00fcller, C., Parent, X., van der Torre, L.: Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artif. Intell. 287, 103348 (2020). https:\/\/doi.org\/10.1016\/j.artint.2020.103348","journal-title":"Artif. Intell."},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-42432-3_6","volume-title":"Mathematical Software \u2013 ICMS 2016","author":"C Benzm\u00fcller","year":"2016","unstructured":"Benzm\u00fcller, C., Scott, D.: Automating free logic in Isabelle\/HOL. In: Greuel, G.-M., Koch, T., Paule, P., Sommese, A. (eds.) ICMS 2016. LNCS, vol. 9725, pp. 43\u201350. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-42432-3_6"},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/s10817-018-09507-7","volume":"64","author":"C Benzm\u00fcller","year":"2020","unstructured":"Benzm\u00fcller, C., Scott, D.S.: Automating free logic in HOL, with an experimental application in category theory. J. Autom. Reason. 64(1), 53\u201372 (2020). https:\/\/doi.org\/10.1007\/s10817-018-09507-7","journal-title":"J. Autom. Reason."},{"key":"5_CR7","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/j.scico.2018.10.008","volume":"172","author":"C Benzm\u00fcller","year":"2019","unstructured":"Benzm\u00fcller, C.: Universal (meta-)logical reasoning: recent successes. Sci. Comput. Program. 172, 48\u201362 (2019). https:\/\/doi.org\/10.1016\/j.scico.2018.10.008","journal-title":"Sci. Comput. Program."},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Ernst, M.: Category theory and foundations. In: Categories for the Working Philosopher, pp. 69\u201389. Oxford University Press (2017). https:\/\/doi.org\/10.1093\/oso\/9780198748991.003.0005","DOI":"10.1093\/oso\/9780198748991.003.0005"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Farmer, W.M.: A partial functions version of church\u2019s simple theory of types. J. Symb. Logic 55(3), 1269\u20131291 (1990). https:\/\/www.jstor.org\/stable\/2274487","DOI":"10.2307\/2274487"},{"key":"5_CR10","unstructured":"Freyd, P., Scedrov, A.: Categories, Allegories, North-Holland Mathematical Library, vol. 39. Elsevier Science (1990). https:\/\/books.google.de\/books?id=fCSJRegkKdoC"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Gabbay, D.M.: Introduction to labelled deductive systems. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 17, pp. 179\u2013266. Springer, Dordrecht (2014). https:\/\/doi.org\/10.1007\/978-94-007-6600-6_3","DOI":"10.1007\/978-94-007-6600-6_3"},{"issue":"1","key":"5_CR12","doi-asserted-by":"publisher","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\u2013101 (1987). https:\/\/doi.org\/10.1016\/0304-3975(87)90045-4","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR13","unstructured":"Katovsky, A.: Category theory. Arch. Formal Proofs 2010 (2010)"},{"issue":"1","key":"5_CR14","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1515\/opphil-2019-0015","volume":"2","author":"D Kirchner","year":"2019","unstructured":"Kirchner, D., Benzm\u00fcller, C., Zalta, E.N.: Computer science and metaphysics: a cross-fertilization. Open Philos. 2(1), 230\u2013251 (2019). https:\/\/doi.org\/10.1515\/opphil-2019-0015","journal-title":"Open Philos."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"MacLane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971)","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1090\/conm\/690\/13872","volume":"690","author":"P Maddy","year":"2017","unstructured":"Maddy, P.: Set-theoretic foundations. Contemp. Math. 690, 289\u2013322 (2017)","journal-title":"Contemp. Math."},{"key":"5_CR17","series-title":"Synthese Library","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-030-15655-8_13","volume-title":"Reflections on the Foundations of Mathematics","author":"P Maddy","year":"2019","unstructured":"Maddy, P.: What do we want a foundation to do? In: Centrone, S., Kant, D., Sarikaya, D. (eds.) Reflections on the Foundations of Mathematics. SL, vol. 407, pp. 293\u2013311. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-15655-8_13"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-030-58285-2_9","volume-title":"KI 2020: Advances in Artificial Intelligence","author":"I Makarenko","year":"2020","unstructured":"Makarenko, I., Benzm\u00fcller, C.: Positive free higher-order logic and its automation via a semantical embedding. In: Schmid, U., Kl\u00fcgl, F., Wolter, D. (eds.) KI 2020. LNCS (LNAI), vol. 12325, pp. 116\u2013131. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58285-2_9"},{"key":"5_CR19","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198533924.001.0001","volume-title":"Elementary Categories","author":"C McLarty","year":"1992","unstructured":"McLarty, C.: Elementary Categories. Elementary Toposes. Clarendon Press, New York (1992)"},{"key":"5_CR20","unstructured":"Melli\u00e8s, P.A.: Categorical semantics of linear logic, pp. 1\u2013196. No. 27 in Panoramas et Synth\u00e8ses, Soci\u00e9t\u00e9 Math\u00e9matique de France (2009)"},{"key":"5_CR21","unstructured":"Milehins, M.: Category theory for ZFC in HOL I: Foundations: Design patterns, set theory, digraphs, semicategories. Archive of Formal Proofs, September 2021. https:\/\/isa-afp.org\/entries\/CZH_Foundations.html, Formal proof development"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Morscher, E., Simons, P.: Free logic: a fifty-year past and an open future. In: Morscher, E., Hieke, A. (eds.) New Essays in Free Logic. In Honour of Karel Lambert, pp. 1\u201334. Springer, Dordrecht (2001). https:\/\/doi.org\/10.1007\/978-94-015-9761-6_1","DOI":"10.1007\/978-94-015-9761-6_1"},{"key":"5_CR23","unstructured":"nLab authors: single-sorted definition of a category, April 2021. https:\/\/ncatlab.org\/nlab\/show\/single-sorted+definition+of+a+category"},{"key":"5_CR24","unstructured":"Nolt, J.: Free logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, Winter 2020 edn. Metaphysics Research Lab, Stanford University (2020)"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Ohlbach, H.J., Nonnengart, A., de Rijke, M., Gabbay, D.M.: Encoding two-valued nonclassical logics in classical logic. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1403\u20131486. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50023-0","DOI":"10.1016\/b978-044450813-3\/50023-0"},{"key":"5_CR26","unstructured":"O\u2019Keefe, G.: Category theory to yoneda\u2019s lemma. Archive of Formal Proofs, April 2005. https:\/\/isa-afp.org\/entries\/Category.html, Formal proof development"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Sch\u00fctte, K.: Syntactical and semantical properties of simple type theory. J. Symb. Logic 25(4), 305\u2013326 (1960). https:\/\/www.jstor.org\/stable\/2963525","DOI":"10.2307\/2963525"},{"key":"5_CR28","unstructured":"Scott, D.: Existence and description in formal logic. In: Schoenman, R., Russell, B. (eds.) Philosopher of the Century, pp. 181\u2013200. George Allen & Unwin, London (1967). Reprinted with additions. In: Lambert, K. (ed.) Philosophical Application of Free Logic, pp. 28\u201348. Oxford University Press (1991)"},{"key":"5_CR29","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/BFb0061839","volume-title":"Applications of Sheaves","author":"D Scott","year":"1979","unstructured":"Scott, D.: Identity and existence in intuitionistic logic. In: Fourman, M., Mulvey, C., Scott, D. (eds.) Applications of Sheaves. LNM, vol. 753, pp. 660\u2013696. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/BFb0061839"},{"key":"5_CR30","unstructured":"Stark, E.W.: Category theory with adjunctions and limits. Archive of Formal Proofs, June 2016. https:\/\/isa-afp.org\/entries\/Category3.html, Formal proof development"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-030-43520-2_19","volume-title":"Relational and Algebraic Methods in Computer Science","author":"L Tiemens","year":"2020","unstructured":"Tiemens, L., Scott, D.S., Benzm\u00fcller, C., Benda, M.: Computer-supported exploration of a categorical axiomatization of modeloids. In: Fahrenberg, U., Jipsen, P., Winter, M. (eds.) RAMiCS 2020. LNCS, vol. 12062, pp. 302\u2013317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43520-2_19"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-42753-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,20]],"date-time":"2023-12-20T10:47:51Z","timestamp":1703069271000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-42753-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031427527","9783031427534"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-42753-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"28 August 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cambridge","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2023\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"52% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}