{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:49Z","timestamp":1774837849997,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540432876","type":"print"},{"value":"9783540458425","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45842-5_12","type":"book-chapter","created":{"date-parts":[[2007,5,27]],"date-time":"2007-05-27T00:00:38Z","timestamp":1180224038000},"page":"181-196","source":"Crossref","is-referenced-by-count":5,"title":["Changing Data Structures in Type Theory: A Study of Natural Numbers"],"prefix":"10.1007","author":[{"given":"Nicolas","family":"Magaud","sequence":"first","affiliation":[]},{"given":"Yves","family":"Bertot","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Penny Anderson. Representing proof transformations for program optimization. In International Conference on Automated Deduction, LNAI 814, Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_42"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Antonia Balaa and Yves Bertot. Fix-point equations for well-founded recursion in type theory. In Harrison and Aagaard [9], pages 1\u201316.","DOI":"10.1007\/3-540-44659-1_1"},{"key":"12_CR3","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin, A. Sa\u03cabi, and B. Werner. The Coq Proof Assistant Reference Manual-Version V6.1. Technical Report 0203, INRIA, August 1997. revised version distributed with Coq."},{"key":"12_CR4","series-title":"Lect Notes Comput Sci","volume-title":"TACS\u201997","author":"S. Boutin","year":"1997","unstructured":"S. Boutin. Using reflection to build efficient and certified decision procedures. In Martin Abadi and Takahashi Ito, editors, TACS\u201997, LNCS 1281, Springer-Verlag, 1997."},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Yann Coscoy. A natural language explanation for formal proofs. In Christian R\u00e9tor\u00e9, editor, Logical Aspects of Computational Linguistics, LNAI 1328, Springer-Verlag, 1996.","DOI":"10.1007\/BFb0052156"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Ewen Denney. A prototype proof translator from HOL to Coq. In Harrison and Aagaard [9], pages 108\u2013125.","DOI":"10.1007\/3-540-44659-1_8"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Amy P. Felty and Douglas J. Howe. Hybrid interactive theorem proving using nuprl and hol. In International Conference on Automated Deduction, number 1249 in LNAI. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_34"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"H. Geuvers, F. Wiedijk, and J. Zwanenburg. Equational reasoning via partial reflection. In Harrison and Aagaard [9], pages 163\u2013179.","DOI":"10.1007\/3-540-44659-1_11"},{"key":"12_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics","year":"1997","unstructured":"J. Harrison and M. Aagaard, editors. Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, LNCS 1869, Springer-Verlag, 2000."},{"key":"12_CR10","unstructured":"Peter Madden. The specialization and transformation of constructive existence proofs. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 131\u2013148. Morgan Kaufmann, 1989."},{"key":"12_CR11","unstructured":"Lena Magnusson. The Implementation of ALF-a Proof Editor based on Martin-L\u00f6f\u2019 s Monomorphic Type Theory with Explicit Substitutions. PhD thesis, Chalmers University of Technology \/ G\u00f6teborg University, 1995."},{"key":"12_CR12","unstructured":"Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999."},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1005936130801","volume":"22","author":"E. Melis","year":"1999","unstructured":"Erica Melis and Jon Whittle. Analogy in inductive theorem proving. Journal of Automated Reasoning, 22:117\u2013147, 1999.","journal-title":"Journal of Automated Reasoning"},{"key":"12_CR14","series-title":"Lect Notes Comput Sci","first-page":"92","volume-title":"Inductive Definitions in the System Coq-Rules and Properties","author":"C. Paulin-Mohring","year":"1993","unstructured":"Christine Paulin-Mohring. Inductive Definitions in the System Coq-Rules and Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference Typed Lambda Calculi and Applications, LNCS 664, Springer-Verlag, 1993. LIP research report 92\u201349."},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Julian Richardson. Automating changes of data type in functional programs. In Proceedings of KBSE-95. IEEE Computer Society, 1995.","DOI":"10.1109\/KBSE.1995.490132"},{"key":"12_CR16","unstructured":"Simon Thompson. Type Theory and functional Programming. Addison-Wesley, 1991."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Philip Wadler. Views: A way for pattern matching to cohabit with data abstraction. In Proceedings, 14th Symposium on Principles of Programming Languages POPL\u201987. ACM, 1987.","DOI":"10.1145\/41625.41653"}],"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-45842-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:03:07Z","timestamp":1556449387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}