{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T05:19:45Z","timestamp":1736486385763,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540406648"},{"type":"electronic","value":"9783540451303"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/10930755_10","type":"book-chapter","created":{"date-parts":[[2006,6,19]],"date-time":"2006-06-19T15:27:09Z","timestamp":1150730829000},"page":"155-170","source":"Crossref","is-referenced-by-count":3,"title":["Embedding of Systems of Affine Recurrence Equations in Coq"],"prefix":"10.1007","author":[{"given":"David","family":"Cachera","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"http: http:\/\/www.irisa.fr\/lande\/pichardie\/coqalpha\/"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44557-9_1","volume-title":"Types for Proofs and Programs","author":"A. Abel","year":"2000","unstructured":"Abel, A.: Specification and verification of a formal system for structurally recursive functions. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 1\u201320. Springer, Heidelberg (2000)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Barthou, D., Feautrier, P., Redon, X.: On the equivalence of two systems of affine recurrence equations. Technical Report 4285, INRIA (2001)","DOI":"10.1007\/3-540-45706-2_40"},{"key":"10_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/3-540-44957-4_42","volume-title":"Computational Logic - CL 2000","author":"R.J. Boulton","year":"2000","unstructured":"Boulton, R.J., Slind, K.: Automatic derivation and application of induction schemes for mutually recursive functions. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 629\u2013643. Springer, Heidelberg (2000)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bove, A.: General Recursion in Type Theory. PhD thesis, Department of Computing Science, Chalmers University of Technology, Sweden (November 2002)","DOI":"10.1007\/3-540-39185-1_3"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Cachera, D., Quinton, P., Rajopadhye, S., Risset, T.: Proving properties of multidimensional recurrences with application to regular parallel algorithms. In: FMPPTA 2001, San Francisco, CA (April 2001)","DOI":"10.1109\/IPDPS.2001.925133"},{"key":"10_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A Tactic Language for the System Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM Journal of Computing (1975)","DOI":"10.1137\/0204006"},{"key":"10_CR9","unstructured":"Filli\u00e2tre, J.-C.: Preuve de programmes imp\u00e9ratifs en th\u00e9orie des types. Th\u00e8se de doctorat, Universit\u00e9 Paris-Sud (July 1999)"},{"issue":"3","key":"10_CR10","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1145\/321406.321418","volume":"14","author":"R.M. Karp","year":"1967","unstructured":"Karp, R.M., Miller, R.E., Winograd, S.: The organization of computations for uniform recurrence equations. Journal of the ACM\u00a014(3), 563\u2013590 (1967)","journal-title":"Journal of the ACM"},{"key":"10_CR11","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":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/BFb0055148","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Nowak","year":"1998","unstructured":"Nowak, D., Beauvais, J.R., Talpin, J.P.: Co-inductive axiomatization of a synchronous language. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 387\u2013399. Springer, Heidelberg (1998)"},{"key":"10_CR13","unstructured":"Pfeifer, H., Dold, A., von Henke, F.W., Ruess, H.: Mechanised semantics of simple imperative programming constructs. Technical Report UIB-96-11, Ulm University (December 1996)"},{"key":"10_CR14","unstructured":"Saouter, Y., Quinton, P.: Computability of Recurrence Equations. Technical Report 1203, IRISA (1990)"},{"key":"10_CR15","unstructured":"LogiCal Project The Coq Development Team. The Coq proof Assistant, Reference Manual"},{"key":"10_CR16","unstructured":"Wilde, D.: A library for doing polyhedral operations. Technical Report 785, Irisa, Rennes, France (1993)"},{"key":"10_CR17","unstructured":"Wilde, D.K.: The Alpha language. Technical Report 999, IRISA, Rennes, France (January 1994)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10930755_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T12:47:34Z","timestamp":1736426854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10930755_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540406648","9783540451303"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/10930755_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}