{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:37:19Z","timestamp":1725557839725},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540406648"},{"type":"electronic","value":"9783540451303"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/10930755_6","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T11:27:09Z","timestamp":1150716429000},"page":"87-102","source":"Crossref","is-referenced-by-count":13,"title":["Changing Data Representation within the Coq System"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Magaud","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44659-1_1","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Balaa","year":"2000","unstructured":"Balaa, A., Bertot, Y.: Fix-point Equations for Well-Founded Recursion in Type Theory. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 1\u201316. Springer, Heidelberg (2000)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45315-6_4","volume-title":"Foundations of Software Science and Computation Structures","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Pons, O.: Type Isomorphisms and Proof Reuse in Dependent Type Theory. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 57\u201371. Springer, Heidelberg (2001)"},{"key":"6_CR3","unstructured":"Bertot, Y., Casteran, P.: Le Coq\u2019Art (2003) (to appear)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Chrzaszcz, J.: Implementation of Modules in the Coq System. Draft (February 2003)","DOI":"10.1007\/10930755_18"},{"key":"6_CR5","unstructured":"Coq development team, INRIA and LRI. The Coq Proof Assistant Reference Manual, Version 7.3 (May 2002)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"C. Cornes","year":"1996","unstructured":"Cornes, C., Terrasse, D.: Automatizing Inversion of Inductive Predicates in Coq. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158. Springer, Heidelberg (1996)"},{"key":"6_CR7","unstructured":"Delahaye, D., Mayero, M.: Field: une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en Coq. In: Cast\u00e9ran, P. (ed.) Journ\u00e9es Francophones des Langages Applicatifs, Pontarlier, Janvier. INRIA (2001)"},{"issue":"4","key":"6_CR8","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive Families. Formal Aspects of Computing\u00a06(4), 440\u2013465 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory. Journal of Symbolic Logic\u00a065(2) (2000)","DOI":"10.2307\/2586554"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/3-540-61780-9_68","volume-title":"Types for Proofs and Programs","author":"M. Hofmann","year":"1996","unstructured":"Hofmann, M.: Conservativity of Equality Reflection over Intensional Type Theory. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 153\u2013165. Springer, Heidelberg (1996)"},{"key":"6_CR11","series-title":"ENTCS","first-page":"23","volume-title":"8th Inter. Conf. on Category Theory in Computer Science (CTCS 1999)","author":"Z. Luo","year":"1999","unstructured":"Luo, Z., Soloviev, S.: Dependent Coercions. In: 8th Inter. Conf. on Category Theory in Computer Science (CTCS 1999), Edinburgh, Scotland. ENTCS, vol.\u00a029, pp. 23\u201334. Elsevier, Amsterdam (1999)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-45842-5_12","volume-title":"Types for Proofs and Programs","author":"N. Magaud","year":"2002","unstructured":"Magaud, N., Bertot, Y.: Changing Data Structures in Type Theory:A Study of Natural Numbers. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 181\u2013196. Springer, Heidelberg (2002)"},{"key":"6_CR13","unstructured":"McBride, C., McKinna, J.: The View from the Left. Journal of Functional Programming, Special Issue: Dependent Type Theory meets Programming Practice (2002) (submitted)"},{"key":"6_CR14","unstructured":"Miquel, A.: Axiom \u2200P,Q: Prop (P \n                    \n                      \n                    \n                    $\\leftrightarrow$\n                   Q)\u2192(P==Q) is safe. Communication in the coq-club list (November 2002)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive Definitions in the System Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664. Springer, Heidelberg (1993); LIP research report 92\u201349"},{"key":"6_CR16","volume-title":"POPL 1997","author":"A. Sa\u00efbi","year":"1997","unstructured":"Sa\u00efbi, A.: Typing Algorithm in Type Theory with Inheritance. In: POPL 1997. ACM, New York (1997)"},{"key":"6_CR17","volume-title":"POPL 1987","author":"P. Wadler","year":"1987","unstructured":"Wadler, P.: Views: A Way for Pattern Matching to Cohabit with Data Abstraction. In: POPL 1987. ACM, New York (1987)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T15:06:27Z","timestamp":1558278387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/10930755_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}