{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:06:50Z","timestamp":1781651210051,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540140313","type":"print"},{"value":"9783540391852","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-39185-1_6","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T20:13:43Z","timestamp":1193429623000},"page":"95-107","source":"Crossref","is-referenced-by-count":13,"title":["Mathematical Quotients and Quotient Types in Coq"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Chicli","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lo\u00efc","family":"Pottier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carlos","family":"Simpson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"F. Barbanera and S. Berardi. Proof-Irrelevance out of Exluded-Middle and Choice in the Calculus of Constructions. Journal of Functional Programming, pages 519\u2013525, 1996.","DOI":"10.1017\/S0956796800001829"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"G. Barthe. Extensions of pure type systems. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of TLCA\u201995, volume 902, pages 16\u201331. Springer-Verlag, 1995.","DOI":"10.1007\/BFb0014042"},{"key":"6_CR3","unstructured":"E. Bishop. Foundations of Constructive Analysis McGraw-Hill, 1967."},{"key":"6_CR4","unstructured":"S. Boutin. R\u00e9flexions sur les quotients. PhD thesis, Th\u00e8se de doctorat, Universit\u00e9 de Paris 7, 1997."},{"key":"6_CR5","unstructured":"Constructive truth in parctice. In H.G. Dales and G. Oliveri, editors, Truth in Mathmatics. Oxford University Press, 1998."},{"key":"6_CR6","unstructured":"The Coq Development Team. The Coq proof assistant V7.3 Reference Manual\n                        \n                  ftp:\/\/ftp.inria.fr\/INRIA\/coq\/V7.3.1\/doc"},{"key":"6_CR7","unstructured":"P. Courtieu. Repr\u00e9sentation d\u2019alg\u00e8bres non libres en th\u00e9orie des types. PhD thesis, Th\u00e8se de doctorat, Universit\u00e9 Paris-Sud, 2001."},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"176","DOI":"10.2307\/2039868","volume":"51","author":"R. Diaconescu","year":"1975","unstructured":"R. Diaconescu. Axiom of choice and complementation. in Proceedings of A.M.S., vol. 51, pages 176\u2013178, 1975.","journal-title":"Proceedings of A.M.S."},{"key":"6_CR9","unstructured":"H. Geuvers. Inconsistency of classical logic in type theory. Note. \n                  http:\/\/www.cs.kun.nl\/herman\/note.ps.gz"},{"key":"6_CR10","unstructured":"M. Hofmann. Extensional concepts in intensional type theory. PhD thesis, LFCS Edinburgh, 1995."},{"key":"6_CR11","unstructured":"S. Lacas and B. Werner. Which choices imply the Excluded Middle? preprint, 1999."},{"key":"6_CR12","series-title":"Lect Notes Comput Sci","first-page":"164","volume-title":"TYPES\u201998","author":"M. E. Maietti","year":"1999","unstructured":"Maria Emilia Maietti. About Effective Quotients in Constructive Type Theory. TYPES\u201998, LNCS 1657, pp 164\u2013178, 1999."},{"key":"6_CR13","unstructured":"Lo\u00efc Pottier. Quotients dans le CCI. Rapport de Recherche INRIA RR-4053. \n                  http:\/\/www-sop.inria.fr\/rapports\/sophia\/RR-4053.html"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-39185-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T15:44:10Z","timestamp":1551023050000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-39185-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540140313","9783540391852"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-39185-1_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]}}}