{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:10:56Z","timestamp":1767928256019,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_17","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"213-228","source":"Crossref","is-referenced-by-count":24,"title":["Pragmatic Quotient Types in Coq"],"prefix":"10.1007","author":[{"given":"Cyril","family":"Cohen","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. Journal of Functional Programming\u00a013(2), 261\u2013293 (2003); Special Issue on Logical Frameworks and Metalanguages","DOI":"10.1017\/S0956796802004501"},{"issue":"1","key":"17_CR2","first-page":"41","volume":"2","author":"M. Sozeau","year":"2009","unstructured":"Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning\u00a02(1), 41\u201362 (2009)","journal-title":"Journal of Formalized Reasoning"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-39185-1_6","volume-title":"Types for Proofs and Programs","author":"L. Chicli","year":"2003","unstructured":"Chicli, L., Pottier, L., Simpson, D.: Mathematical quotients and quotient types in Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 95\u2013107. Springer, Heidelberg (2003)"},{"key":"17_CR4","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A small scale reflection extension for the Coq system. INRIA Technical report, \n                    \n                      http:\/\/hal.inria.fr\/inria-00258384"},{"key":"17_CR5","unstructured":"The Mathematical Components Project: SSReflect extension and libraries, \n                    \n                      http:\/\/www.msr-inria.inria.fr\/Projects\/math-components\/index_html"},{"key":"17_CR6","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.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"key":"17_CR7","unstructured":"Cohen, C.: Formalized algebraic numbers: construction and first order theory. PhD thesis, \u00c9cole polytechnique (2012)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Saibi, A.: Typing algorithm in type theory with inheritance. In: Proceedings of Principles of Programming Languages, POPL 1997, pp. 292\u2013301 (1997)","DOI":"10.1145\/263699.263742"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Hedberg, M.: A coherence theorem for Martin-L\u00f6f\u2019s type theory. Journal of Functional Programming, 4\u20138 (1998)","DOI":"10.1017\/S0956796898003153"},{"key":"17_CR10","unstructured":"Bartzia, I., Strub, P.Y.: A formalization of elliptic curves (2011), \n                    \n                      http:\/\/pierre-yves.strub.nu\/research\/ec\/"},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.jalgebra.2013.01.016","volume":"381","author":"C. Cohen","year":"2013","unstructured":"Cohen, C., Coquand, T.: A constructive version of laplace\u2019s proof on the existence of complex roots. Journal of Algebra\u00a0381, 110\u2013115 (2013)","journal-title":"Journal of Algebra"},{"key":"17_CR12","unstructured":"Cohen, C.: Reasoning about big enough numbers in Coq (2012), \n                    \n                      http:\/\/perso.crans.org\/cohen\/work\/bigenough\/"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-32347-8_6","volume-title":"Interactive Theorem Proving","author":"C. Cohen","year":"2012","unstructured":"Cohen, C.: Construction of real algebraic numbers in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 67\u201382. Springer, Heidelberg (2012)"},{"key":"17_CR14","unstructured":"Hofmann, M.: Extensional concepts in intensional type theory. Phd thesis, University of Edinburgh (1995)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"554","DOI":"10.1007\/3-540-44802-0_39","volume-title":"Computer Science Logic","author":"P. Courtieu","year":"2001","unstructured":"Courtieu, P.: Normalized types. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 554\u2013569. Springer, Heidelberg (2001)"},{"key":"17_CR16","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A Modular Formalisation of Finite Group Theory. Rapport de recherche RR-6156, INRIA (2007)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:50:24Z","timestamp":1558317024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}