{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T05:48:54Z","timestamp":1784180934462,"version":"3.55.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030535179","type":"print"},{"value":"9783030535186","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_4","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"55-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Leveraging the Information Contained in Theory Presentations"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Carette","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"William M.","family":"Farmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yasmine","family":"Sharoda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Al-hassy, M., Carette, J., Kahl, W.: A language feature to unbundle data at will (short paper). In: Proceedings of the 18th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, GPCE 2019, pp. 14\u201319. ACM, New York (2019)","DOI":"10.1145\/3357765.3359523"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Bl\u00f6ndal, B., L\u00f6h, A., Scott, R.: Deriving via: or, how to turn hand-written instances into an anti-pattern. In: Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell 2018, pp. 55\u201367. Association for Computing Machinery, New York (2018)","DOI":"10.1145\/3242744.3242746"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-48256-3_10","volume-title":"Theorem Proving in Higher Order Logics","author":"V Capretta","year":"1999","unstructured":"Capretta, V.: Universal algebra in type theory. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 131\u2013148. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_10"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Carette, J., Elsheikh, M., Smith, S.: A generative geometric kernel. In: Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 53\u201362. ACM (2011)","DOI":"10.1145\/1929501.1929510"},{"key":"4_CR5","unstructured":"Carette, J., et al.: The MathScheme library: Some preliminary experiments. arXiv preprint arXiv:1106.1862, June 2011"},{"key":"4_CR6","unstructured":"Carette, J., Farmer, W.M., Kohlhase, M., Rabe, F.: Big math and the one-brain barrier a position paper and architecture proposal. arXiv preprint arXiv:1904.10405 (2019)"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1017\/S0956796809007205","volume":"19","author":"J Carette","year":"2009","unstructured":"Carette, J., Kiselyov, O., Shan, C.: Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages. J. Funct. Program. 19(5), 509\u2013543 (2009)","journal-title":"J. Funct. Program."},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-31374-5_14","volume-title":"Intelligent Computer Mathematics","author":"J Carette","year":"2012","unstructured":"Carette, J., O\u2019Connor, R.: Theory presentation combinators. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 202\u2013215. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31374-5_14"},{"key":"4_CR9","unstructured":"Carette, J., O\u2019Connor, R., Sharoda, Y.: Building on the diamonds between theories: theory presentation combinators. arXiv preprint arXiv:1812.08079 (2018)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic, vol. 4, pp. 65\u201389 (1996)","DOI":"10.1016\/S1571-0661(04)00034-9"},{"key":"4_CR11","unstructured":"Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi. https:\/\/hal.inria.fr\/hal-02478907 (2020). working paper or preprint"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"The Mathlib Community. The lean mathematical library. arXiv preprint arXiv: 1910.09336 (2019).","DOI":"10.1145\/3372885.3373824"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"NG de Bruijn","year":"1991","unstructured":"de Bruijn, N.G.: Telescopic mappings in typed lambda calculus. Inf. Comput. 91(2), 189\u2013204 (1991)","journal-title":"Inf. Comput."},{"key":"4_CR14","volume-title":"Universal Algebra and Applications in Theoretical Computer Science","author":"K Denecke","year":"2002","unstructured":"Denecke, K., Wismath, S.L.: Universal Algebra and Applications in Theoretical Computer Science. Taylor & Francis, New York (2002)"},{"key":"4_CR15","series-title":"Monographs in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1: Equations and Initial Semantics","author":"H Ehrig","year":"2012","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-69962-7"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/3-540-55602-8_192","volume-title":"Automated Deduction\u2014CADE-11","author":"WM Farmer","year":"1992","unstructured":"Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567\u2013581. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_192"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"issue":"4","key":"4_CR18","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput. 34(4), 271\u2013286 (2002)","journal-title":"J. Symb. Comput."},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-08970-6_18","volume-title":"Interactive Theorem Proving","author":"J Gross","year":"2014","unstructured":"Gross, J., Chlipala, A., Spivak, D.I.: Experience implementing a performant category-theory library in Coq. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 275\u2013291. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_18"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/j.entcs.2018.10.010","volume":"338","author":"E Gunther","year":"2018","unstructured":"Gunther, E., Gadea, A., Pagano, M.: Formalization of universal algebra in Agda. Electron. Not. Theor. Comput. Sci. 338, 147\u2013166 (2018). The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017)","journal-title":"Electron. Not. Theor. Comput. Sci."},{"key":"4_CR21","unstructured":"Halleck, J.: Logic system interrelationships. http:\/\/www.horizons-2000.org\/2.%20Ideas%20and%20Meaning\/John%20Halleck%27s%20Logic%20System%20Interrelationships.html. Accessed 20 Mar 2020"},{"key":"4_CR22","unstructured":"Haskell; an advanced, purely functional programming language. https:\/\/www.haskell.org\/. Accessed 22 Mar 2020"},{"key":"4_CR23","unstructured":"Jipsen, P.: List of mathematical structures. http:\/\/math.chapman.edu\/~jipsen\/structures\/doku.php. Accessed 20 Mar 2020"},{"key":"4_CR24","unstructured":"Haskell lens library. https:\/\/hackage.haskell.org\/package\/lens. version 4.19.1. Accessed 22 Mar 2020"},{"issue":"11","key":"4_CR25","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/2088456.1863529","volume":"45","author":"JP Magalh\u00e3es","year":"2010","unstructured":"Magalh\u00e3es, J.P., Dijkstra, A., Jeuring, J., L\u00f6h, A.: A generic deriving mechanism for Haskell. ACM SIGPLAN Not. 45(11), 37\u201348 (2010)","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR26","unstructured":"Mazzoli, F., Abel, A.: Type checking through unification. arXiv preprint arXiv:1609.09709 (2016)"},{"key":"4_CR27","unstructured":"Mazzoli, F., Danielsson, N.A., Norell, U., Vezzosi, A., Abel, A.: Tog, a prototypical implementation of dependent types. https:\/\/github.com\/bitonic\/tog"},{"issue":"2","key":"4_CR28","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1016\/0304-3975(92)90310-C","volume":"100","author":"K Meinke","year":"1992","unstructured":"Meinke, K.: Universal algebra in higher types. Theor. Comput. Sci. 100(2), 385\u2013417 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Meinke, K., Tucker, J.V.: Universal algebra. University of Wales (Swansea). Mathematics and Computer Science Division (1991)","DOI":"10.1007\/3-540-54496-8_10"},{"key":"4_CR30","unstructured":"Pottier, L.: Coq user contributions - algebra library. https:\/\/github.com\/coq-contribs\/algebra"},{"key":"4_CR31","series-title":"Graduate Texts Math","volume-title":"A Course in Universal Algebra","author":"HP Sankappanavar","year":"1981","unstructured":"Sankappanavar, H.P., Burris, S.: A Course in Universal Algebra. Graduate Texts Math, vol. 78. Springer, New York (1981)"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Sannella, D., Tarlecki, A.: Universal algebra. In: Foundations of Algebraic Specification and Formal Software Development. Monographs in Theoretical Computer Science. An EATCS Series, pp. 15\u201339. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-17336-3_1","DOI":"10.1007\/978-3-642-17336-3_1"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Sheard, T., Jones, S.P.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell 2002, pp. 1\u201316. Association for Computing Machinery, New York (2002)","DOI":"10.1145\/581690.581691"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/978-3-642-14052-5_35","volume-title":"Interactive Theorem Proving","author":"B Spitters","year":"2010","unstructured":"Spitters, B., van der Weegen, E.: Developing the algebraic hierarchy with type classes in Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 490\u2013493. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_35"},{"key":"4_CR35","unstructured":"Whitehead, A.N.: A Treatise on Universal Algebra: With Applications. Cornell University Library Historical Math Monographs. The University Press (1898)"}],"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-030-53518-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,23]],"date-time":"2021-04-23T23:15:40Z","timestamp":1619219740000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","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":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/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":"35","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":"15","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":"9","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":"43% - 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-4","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)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}