{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:51:41Z","timestamp":1725544301527},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540334385"},{"type":"electronic","value":"9783540334392"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11737414_9","type":"book-chapter","created":{"date-parts":[[2006,3,15]],"date-time":"2006-03-15T11:54:37Z","timestamp":1142423677000},"page":"114-129","source":"Crossref","is-referenced-by-count":30,"title":["Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Julien","family":"Forest","sequence":"additional","affiliation":[]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[]},{"given":"Vlad","family":"Rusu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_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":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45685-6_4","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Barthe","year":"2002","unstructured":"Barthe, G., Courtieu, P.: Efficient Reasoning about Executable Specifications in Coq. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 31\u201346. Springer, Heidelberg (2002)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 302\u2013319. Springer, Heidelberg (2001)"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1017\/S0960129503004122","volume":"14","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., Frade, M.J., Gim\u00e9nez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science\u00a014, 97\u2013141 (2004)","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/3-540-45685-6_7","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2002","unstructured":"Bertot, Y., Capretta, V., Das Barman, K.: Type-theoretic functional semantics. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 83\u201398. Springer, Heidelberg (2002)"},{"key":"9_CR7","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development\u2014 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2014 Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"issue":"1","key":"9_CR8","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1017\/S0960129504004426","volume":"15","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science\u00a015(1), 37\u201392 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1017\/S0960129505004822","volume":"15","author":"A. Bove","year":"2005","unstructured":"Bove, A., Capretta, V.: Modelling general recursion in type theory. Mathematical Structures in Computer Science\u00a015, 671\u2013708 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Cachera, D., Jensen, T., Pichardie, D., Rusu, V.: Extracting a data flow analyzer in constructive logic. Theoretical Computer Science\u00a0342 (2005) (to appear)","DOI":"10.1016\/j.tcs.2005.06.004"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/10930755_10","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cachera","year":"2003","unstructured":"Cachera, D., Pichardie, D.: Embedding of Systems of Affine Recurrence Equations in Coq. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 155\u2013170. Springer, Heidelberg (2003)"},{"issue":"2","key":"9_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-1(2:1)2005","volume":"1","author":"V. Capretta","year":"2005","unstructured":"Capretta, V.: General recursion via coinductive types. Logical Methods in Computer Science\u00a01(2), 1\u201318 (2005)","journal-title":"Logical Methods in Computer Science"},{"key":"9_CR13","unstructured":"Coq Development Team. The Coq Proof Assistant User\u2019s Guide. Version 8.0 (January 2004)"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"525","DOI":"10.2307\/2586554","volume":"65","author":"P. Dybjer","year":"2000","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic\u00a065(2), 525\u2013549 (2000)","journal-title":"Journal of Symbolic Logic"},{"volume-title":"Introduction to HOL: A theorem proving environment for higher-order logic","year":"1993","key":"9_CR15","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/11541868_7","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Gr\u00e9goire","year":"2005","unstructured":"Gr\u00e9goire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in coq. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 98\u2013113. Springer, Heidelberg (2005)"},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1109\/82.749082","volume":"46","author":"M. Katsushige","year":"1999","unstructured":"Katsushige, M., Kiyoshi, N., Hitoshi, K.: Pipelined LMS Adaptative Filter Using a New Look-Ahead Transformation. IEEE Transactions on Circuits and Systems\u00a046, 51\u201355 (1999)","journal-title":"IEEE Transactions on Circuits and Systems"},{"key":"9_CR18","volume-title":"Proceedings of POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of POPL 2006. ACM Press, New York (2006)"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming\u00a014, 69\u2013111 (2004)","journal-title":"Journal of Functional Programming"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"3","key":"9_CR21","doi-asserted-by":"publisher","first-page":"605","DOI":"10.1007\/BF01941137","volume":"28","author":"B. Nordstr\u00f6m","year":"1988","unstructured":"Nordstr\u00f6m, B.: Terminating general recursion. BIT\u00a028(3), 605\u2013619 (1988)","journal-title":"BIT"},{"key":"9_CR22","unstructured":"Color Project, \n                      \n                        http:\/\/color.inria.fr"},{"key":"#cr-split#-9_CR23.1","unstructured":"Shankar, N., Owre, S., Rushby, J.M.: The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International (February 1993);"},{"key":"#cr-split#-9_CR23.2","unstructured":"Supplemented with the PVS2 Quick Reference Manual (1997)"},{"key":"9_CR24","unstructured":"Slind, K.: Reasoning about Terminating Functional Programs. PhD thesis, TU M\u00fcnich (1999)"},{"issue":"1","key":"9_CR25","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/A:1019916231463","volume":"15","author":"H. Xi","year":"2002","unstructured":"Xi, H.: Dependent types for program termination verification. Higher-Order and Symbolic Computation\u00a015(1), 91\u2013131 (2002)","journal-title":"Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11737414_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T03:28:28Z","timestamp":1552361308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11737414_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540334385","9783540334392"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11737414_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}