{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:44:02Z","timestamp":1767926642865,"version":"3.49.0"},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T00:00:00Z","timestamp":1309478400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2011,8]]},"abstract":"<jats:p>The introduction of first-class type classes in the Coq system calls for a re-examination of the basic interfaces used for mathematical formalisation in type theory. We present a new set of type classes for mathematics and take full advantage of their unique features to make practical a particularly flexible approach that was formerly thought to be unfeasible. Thus, we address traditional proof engineering challenges as well as new ones resulting from our ambition to build upon this development a library of constructive analysis in which any abstraction penalties inhibiting efficient computation are reduced to a minimum.<\/jats:p><jats:p>The basis of our development consists of type classes representing a standard algebraic hierarchy, as well as portions of category theory and universal algebra. On this foundation, we build a set of mathematically sound abstract interfaces for different kinds of numbers, succinctly expressed using categorical language and universal algebra constructions. Strategic use of type classes lets us support these high-level theory-friendly definitions, while still enabling efficient implementations unhindered by gratuitous indirection, conversion or projection.<\/jats:p><jats:p>Algebra thrives on the interplay between syntax and semantics. The Prolog-like abilities of type class instance resolution allow us to conveniently define a quote function, thus facilitating the use of reflective techniques.<\/jats:p>","DOI":"10.1017\/s0960129511000119","type":"journal-article","created":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T14:53:35Z","timestamp":1309532015000},"page":"795-825","source":"Crossref","is-referenced-by-count":54,"title":["Type classes for mathematics in type theory"],"prefix":"10.1017","volume":"21","author":[{"given":"BAS","family":"SPITTERS","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"EELIS","family":"VAN DER WEEGEN","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2011,7,1]]},"reference":[{"key":"S0960129511000119_ref1","first-page":"83","volume-title":"Proceedings, Interactive Theorem Proving, ITP 2010","author":"Armand","year":"2010"},{"key":"S0960129511000119_ref37","first-page":"2615","article-title":"Type systems for computer algebra","volume":"10","author":"Weber","year":"1993","journal-title":"Relation"},{"key":"S0960129511000119_ref11","unstructured":"Coq Development Team (2008) The Coq Proof Assistant Reference Manual, INRIA-Rocquencourt."},{"key":"S0960129511000119_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0960129511000119_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.10.001"},{"key":"S0960129511000119_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9070-5"},{"key":"S0960129511000119_ref28","unstructured":"Palmgren E. (2009) Constructivist and Structuralist Foundations: Bishops and Lawveres Theories of Sets. Technical Report 4."},{"key":"S0960129511000119_ref21","volume-title":"AXIOM: the scientific computation system","author":"Jenks","year":"1992"},{"key":"S0960129511000119_ref25","first-page":"189","volume-title":"Handbook of logic in computer science (volume 1)","author":"Meinke","year":"1993"},{"key":"S0960129511000119_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0963-1"},{"key":"S0960129511000119_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68103-8_11"},{"key":"S0960129511000119_ref22","volume-title":"Categories for the working mathematician","author":"Mac Lane","year":"1998"},{"key":"S0960129511000119_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-18317-5_20"},{"key":"S0960129511000119_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02614-0_10"},{"key":"S0960129511000119_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_8"},{"key":"S0960129511000119_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"S0960129511000119_ref6","volume-title":"Foundations of constructive analysis","author":"Bishop","year":"1967"},{"key":"S0960129511000119_ref14","first-page":"88","volume-title":"Proceedings of MKM2004","author":"Cruz-Filipe","year":"2004"},{"key":"S0960129511000119_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"S0960129511000119_ref10","unstructured":"Cartmell J. (1978) Generalized algebraic theories and contextual categories, Ph.D. thesis, University of Oxford."},{"key":"S0960129511000119_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"S0960129511000119_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"S0960129511000119_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85110-3_23"},{"key":"S0960129511000119_ref17","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2002.0552"},{"key":"S0960129511000119_ref18","first-page":"153","volume-title":"Types for Proofs and Programs International Conference, TYPES 2008","author":"Haftmann","year":"2008"},{"key":"S0960129511000119_ref23","first-page":"153","article-title":"Constructive mathematics and computer programming","volume":"104","author":"Martin-L\u00f6f","year":"1982","journal-title":"Logic, methodology and philosophy of science, VI"},{"key":"S0960129511000119_ref24","first-page":"127","volume-title":"Twenty-five years of constructive type theory","author":"Martin-L\u00f6f","year":"1998"},{"key":"S0960129511000119_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_21"},{"key":"S0960129511000119_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.05.031"},{"key":"S0960129511000119_ref30","first-page":"39","volume-title":"Handbook of Logic in Computer Science: Logic and algebraic methods (volume 5)","author":"Pitts","year":"2001"},{"key":"S0960129511000119_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200018"},{"key":"S0960129511000119_ref33","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1995.1006"},{"key":"S0960129511000119_ref34","first-page":"41","article-title":"A new look at generalized rewriting in type theory.","volume":"2","author":"Sozeau","year":"2009","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129511000119_ref38","unstructured":"Zumkeller R. (2008) Global Optimization in Type Theory, Ph.D. thesis, \u00c9cole Polytechnique, Paris."},{"key":"S0960129511000119_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004501"},{"key":"S0960129511000119_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_10"},{"key":"S0960129511000119_ref20","unstructured":"Huet G. and Saibi A. (1995) Constructive category theory. In: Proceedings of the Joint CLICS-TYPES Workshop on Categories and Type Theory, G\u00f6teborg."},{"key":"S0960129511000119_ref36","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/75277.75283","volume-title":"Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"Wadler","year":"1989"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129511000119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T22:42:30Z","timestamp":1686177750000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129511000119\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,1]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011,8]]}},"alternative-id":["S0960129511000119"],"URL":"https:\/\/doi.org\/10.1017\/s0960129511000119","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,7,1]]}}}