{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:49:53Z","timestamp":1725475793164},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"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":[[2000]]},"DOI":"10.1007\/10721959_4","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"45-63","source":"Crossref","is-referenced-by-count":5,"title":["Wellfounded Schematic Definitions"],"prefix":"10.1007","author":[{"given":"Konrad","family":"Slind","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Anderson, P., Basin, D.: Program development schemata as derived rules. Journal of Symbolic Computation (2000) (to appear)","DOI":"10.1006\/jsco.1999.0346"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/3-540-15975-4_48","volume-title":"Functional Programming Languages and Computer Architecture","author":"L. Augustsson","year":"1985","unstructured":"Augustsson, L.: Compiling pattern matching. In: Jouannnaud, J.P. (ed.) Functional Programming and Computer Architecture LNCS, vol.\u00a0201, pp. 368\u2013381. Springer, Heidelberg (1985)"},{"key":"4_CR3","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Coscoy, Y., Delahaye, D., Rauglaudre, D.d., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Laulhere, H., Munoz, C., Murthy, C., Parent-Vigouroux, C., Loiseleur, P., Mohring, C.P., Saibi, A., Werner, B.: The Coq Proof Assistant Reference Manual. In: INRIA, 6th edn (December 1999) accessible at, \n                    \n                      http:\/\/pauillac.inria.fr\/coq\/doc\/main.html"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","first-page":"17","volume-title":"Mathematics of Program Construction","author":"R. Bird","year":"1995","unstructured":"Bird, R.: Functional algorithm design. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol.\u00a0947, pp. 17\u201321. Springer, Heidelberg (1995)"},{"key":"4_CR5","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)"},{"issue":"1","key":"4_CR6","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. Burstall","year":"1977","unstructured":"Burstall, R., Darlington, J.: A transformation system for developing recursive programs. Journal of the Association for Computing Machinery\u00a024(1), 44\u201367 (1977)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A formulation of the Simple Theory of Types. Journal of Symbolic Logic\u00a05, 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"issue":"8","key":"4_CR8","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. CACM\u00a022(8), 465\u2013476 (1979)","journal-title":"CACM"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-60043-4_69","volume-title":"Algebraic Methodology and Software Technology","author":"A. Dold","year":"1995","unstructured":"Dold, A.: Representing, verifying and applying software development steps using the PVS system. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol.\u00a0936, pp. 431\u2013435. Springer, Heidelberg (1995)"},{"key":"4_CR10","unstructured":"Dold, A.: Software development in PVS using generic development steps. In: Proceedings of a Seminar on Generic Programming (April 1998) (to appear in Springer LNCS)"},{"key":"4_CR11","unstructured":"Farmer, W.: Recursive definitions in IMPS (1997) (available by anonymous FTP at ftp.harvard.edu, in directory imps\/doc, file name recursivedefinitions. dvi.gz)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/3-540-49674-2_7","volume-title":"Logic Program Synthesis and Transformation","author":"P. Flener","year":"1998","unstructured":"Flener, P., Lau, K.-K., Ornaghi, M.: On correct program schemas. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol.\u00a01463, pp. 124\u2013143. Springer, Heidelberg (1998)"},{"key":"4_CR13","volume-title":"Introduction to HOL, a theorem proving environment for higher order logic","author":"M. Gordon","year":"1993","unstructured":"Gordon, M., Melham, T.: Introduction to HOL, a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)"},{"key":"4_CR14","unstructured":"Hardware Verification Group. Hol98 User\u2019s Manual. University of Cambridge (December 1999) accessible at, \n                    \n                      http:\/\/www.ftp.cl.cam.ac.uk\/ftp\/hvg\/hol98"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-60275-5_66","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"J. Harrison","year":"1995","unstructured":"Harrison, J.: Inductive definitions: automation and application. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol.\u00a0971, pp. 200\u2013213. Springer, Heidelberg (1995)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL-Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"4_CR17","volume-title":"CPHC\/BCS Distinguished Dissertations","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. In: CPHC\/BCS Distinguished Dissertations. Springer, Heidelberg (1998)"},{"key":"4_CR18","first-page":"31","volume":"11","author":"G. Huet","year":"1978","unstructured":"Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Informatica\u00a011, 31\u201355 (1978)","journal-title":"Informatica"},{"key":"4_CR19","volume-title":"ACM Symposium on Principles of Programming Languages","author":"J.R. Lewis","year":"2000","unstructured":"Lewis, J.R., Shields, M.B., Meijer, E., Launchbury, J.: Implicit parameters: Dynamic scoping with static types. In: Reps, T. (ed.) ACM Symposium on Principles of Programming Languages, Boston, Massachusetss, USA. ACM Press, New York (2000)"},{"key":"4_CR20","unstructured":"Maranget, L.: Two techniques for compiling lazy pattern matching. Technical Report 2385, INRIA (October 1994)"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1109\/HOL.1991.596299","volume-title":"Proceedings of the 1991 InternationalWorkshop on the HOL Theorem Proving System and its Applications","author":"T. Melham","year":"1991","unstructured":"Melham, T.: A package for inductive relation definitions in HOL. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) Proceedings of the 1991 InternationalWorkshop on the HOL Theorem Proving System and its Applications, pp. 350\u2013357. IEEE Computer Society Press, Davis, California, USA (1991)"},{"key":"4_CR22","unstructured":"Owre, S., Rushby, J.M., Shankar, N., Stringer-Calvert, D.J.: PVS Sys- tem Guide. SRI Computer Science Laboratory (September 1998) available at, \n                    \n                      http:\/\/pvs.csl.sri.com\/manuals.html"},{"key":"4_CR23","volume-title":"Texts and Monographs in Computer Science","author":"H.A. Partsch","year":"1990","unstructured":"Partsch, H.A.: Specification and Transformation of Programs: A Formal Approach to Software Development. In: Texts and Monographs in Computer Science. Springer, Heidelberg (1990)"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/3-540-58156-1_11","volume-title":"Automated Deduction - CADE-12","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: A fixedpoint approach to implementing (co)inductive definitions. In: Bundy, A. (ed.) CADE 1994. LNCS(LNAI), vol.\u00a0814, pp. 148\u2013161. Springer, Heidelberg (1994)revised version available at, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/users\/lcp\/papers\/recur.html\n                    \n                    \n                   under title \u2018A Fixedpoint Approach to (Co)inductive and Co(datatype) Definitions\u2019"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle : A Generic Theorem Prover","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994) up-to-date reference manual can be found at, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/dist\/"},{"issue":"2- 3","key":"4_CR26","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/S0167-6423(96)00023-8","volume":"8","author":"P. Pepper","year":"1997","unstructured":"Pepper, P., Smith, D.R.: A high-level derivation of global search algorithms (with constraint propagation). Science of Computer Programming\u00a08(2- 3), 247\u2013271 (1997)","journal-title":"Science of Computer Programming"},{"key":"4_CR27","unstructured":"Persson, H.: Type Theory and the Integrated Logic of Programs. PhD thesis. Chalmers University of Technology (June 1999)"},{"issue":"3","key":"4_CR28","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1023\/A:1006218513245","volume":"23","author":"P. Rudnicki","year":"1999","unstructured":"Rudnicki, P., Trybulec, A.: On equivalents of well-foundedness. Journal of Automated Reasoning\u00a023(3), 197\u2013234 (1999)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-60117-1_5","volume-title":"Mathematics of Program Construction","author":"N. Shankar","year":"1995","unstructured":"Shankar, N.: Steps towards mechanizing program transformations using PVS. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol.\u00a0947, pp. 50\u201366. Springer, Heidelberg (1995)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1996","unstructured":"Slind, K.: Function definition in higher order logic. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125. Springer, Heidelberg (1996)"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028400","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"1997","unstructured":"Slind, K.: Derivation and use of induction sche mes in higher order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275. Springer, Heidelberg (1997)"},{"key":"4_CR32","unstructured":"Slind, K.: Reasoning about Terminating Functional Programs. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (1999) accessible at, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/users\/kxs\/papers"},{"issue":"27","key":"4_CR33","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1145\/322169.322183","volume":"1","author":"M. Wand","year":"1980","unstructured":"Wand, M.: Continuation-based program transformation strategies. Journal of the ACM\u00a01(27), 164\u2013180 (1980)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T23:31:25Z","timestamp":1558308685000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/10721959_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}