{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:19:23Z","timestamp":1725455963875},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556312"},{"type":"electronic","value":"9783540472650"}],"license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/bfb0021083","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T05:35:18Z","timestamp":1132637718000},"page":"58-70","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Development transformation based on higher order type theory"],"prefix":"10.1007","author":[{"given":"Jianguo","family":"Lu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiafu","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,16]]},"reference":[{"unstructured":"N.G.de Bruijn, A Survey of the Project AUTOMATH, in: J.P.Seldin and J.R.Hindley (editors), To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Prentice Hall, 1980.","key":"5_CR1"},{"doi-asserted-by":"crossref","unstructured":"R.M.Burstall, Transformational System for Developing R ecursive Programs, JACM 24(1), pp.44\u201367.","key":"5_CR2","DOI":"10.1145\/321992.321996"},{"unstructured":"J.Carbonell, Derivational Analogy: A Theory of Reconstructive Problem Solving and Expertise Acquisition, in R.S. Michalski et al(ed.), Machine Intelligence: An Artificial Intelligence Approach, Morgan Kaufmann, 1986.","key":"5_CR3"},{"unstructured":"R. Constable, et al, Implementing Mathematics with NuPRL Proof Development System, Prentice Hall, 1985.","key":"5_CR4"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(81)90014-X","volume":"16","author":"J. Darlington","year":"1981","unstructured":"John Darlington, An Experimental Program transformation and Synthesis System, Artificial Intelligence 16(1981), pp. 1\u201346.","journal-title":"Artificial Intelligence"},{"unstructured":"Nachum Dershowitz, Programming By Analogy, in R.S.Michalski et al (eds.), Machine Learning II: An Artificial Intelligence Approach,Morgan Kaufmann, 1986.","key":"5_CR6"},{"unstructured":"R. Harper, F.A.Honsell, G.Plotkin, A Framework for Defining Logics, Proceedings of the second symposium on Logic in Computer Science, PP. 194\u2013204, IEEE, 1986.","key":"5_CR7"},{"unstructured":"W.A.Howard, The Formula as Types Notion of Construction, in: J.P.Seldin and J.R.Hindley (editors), To H.B.Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Prentice Hall, 1980.","key":"5_CR8"},{"unstructured":"Jianguo Lu, Research on Analogical Program Derivation Based on Type Theory, Ph.D. Dissertation, Nanjing University, 1991.","key":"5_CR9"},{"key":"5_CR10","volume-title":"Automatic Programming Optimization via the Transformation of NuPRL Synthesis Proofs","author":"P. Madden","year":"1988","unstructured":"P.Madden, Automatic Programming Optimization via the Transformation of NuPRL Synthesis Proofs, UK IT 88 Conference Publication, Swansea, UK, 4\u20137 July, 1988."},{"doi-asserted-by":"crossref","unstructured":"Per Martin-Lof, Constructive Mathematics and Computer Programming, in Logic, Methodology and Philosophy of Science, pp.153\u2013175, North Holland, 1982.","key":"5_CR11","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0004-3702(89)90048-9","volume":"40","author":"J. Mostow","year":"1989","unstructured":"J. Mostow, Design by Derivational Analogy: Issues in the Automated Replay of Design Plans, Artificial Intelligence 40(1989), pp.119\u2013184.","journal-title":"Artificial Intelligence"},{"doi-asserted-by":"crossref","unstructured":"R.P.Nederpelt, An approach to theorem proving on the basis of typed lambda calculus, 5th Conference on Automated Deduction, LNCS 87, pp.181\u2013190, 1980.","key":"5_CR13","DOI":"10.1007\/3-540-10009-1_15"},{"doi-asserted-by":"crossref","unstructured":"M. Sintzoff, Understanding and Expressing Software Construction, in P.Pepper(ed.), Program Transformation and Programming Environment, Springer, 1984.","key":"5_CR14","DOI":"10.1007\/978-3-642-46490-4_16"},{"unstructured":"M. Weber, A Meta Calculus for Formal System Development, Ph.D. Dissertation, der Universitat Karlsruhe, 1990.","key":"5_CR15"},{"unstructured":"Jiafu Xu, Reports on a Software Automation R & D Project, Information Processing '89, G.X.Ritter(ed.), Elsevier Science Publisher, B.V.(North-Holland), Aug. 1989.","key":"5_CR16"}],"container-title":["Lecture Notes in Computer Science","Constructivity in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0021083","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T14:31:49Z","timestamp":1683297109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0021083"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556312","9783540472650"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0021083","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]},"assertion":[{"value":"16 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}