{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T08:54:32Z","timestamp":1778662472522,"version":"3.51.4"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,3,7]],"date-time":"2017-03-07T00:00:00Z","timestamp":1488844800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/J017515\/1"],"award-info":[{"award-number":["EP\/J017515\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s10817-017-9409-5","type":"journal-article","created":{"date-parts":[[2017,3,7]],"date-time":"2017-03-07T14:23:44Z","timestamp":1488896624000},"page":"157-176","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Genetic Programming $$\\varvec{+}$$ + Proof Search $$\\varvec{=}$$ = Automatic Improvement"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5542-4156","authenticated-orcid":false,"given":"Zoltan A.","family":"Kocsis","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1944-7147","authenticated-orcid":false,"given":"Jerry","family":"Swan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,7]]},"reference":[{"issue":"3","key":"9409_CR1","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1109\/MS.2001.922739","volume":"18","author":"RL Glass","year":"2001","unstructured":"Glass, R.L.: Frequently forgotten fundamental facts about software engineering. IEEE Softw. 18(3), 112\u2013111 (2001)","journal-title":"IEEE Softw."},{"key":"9409_CR2","doi-asserted-by":"crossref","first-page":"421","DOI":"10.1007\/s11219-013-9208-0","volume":"21","author":"C Goues Le","year":"2013","unstructured":"Le Goues, C., Forrest, S., Weimer, W.: Current challenges in automatic software repair. Softw. Qual. J. 21, 421\u2013443 (2013)","journal-title":"Softw. Qual. J."},{"key":"9409_CR3","unstructured":"Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection (Complex Adaptive Systems), 1st edn. MIT Press, Cambridge (1992)"},{"issue":"5","key":"9409_CR4","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1145\/1735223.1735249","volume":"53","author":"W Weimer","year":"2010","unstructured":"Weimer, W., Forrest, S., Le Goues, C., Nguyen, T.: Automatic program repair with evolutionary computation. Commun. ACM 53(5), 109\u2013116 (2010)","journal-title":"Commun. ACM"},{"key":"9409_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-662-44303-3_12","volume-title":"Genetic Programming","author":"J Petke","year":"2014","unstructured":"Petke, J., Harman, M., Langdon, W.B., Weimer, W.: Using genetic improvement and code transplants to specialise a C++ program to a problem class. In: Nicolau, M., Krawiec, K., Heywood, M.I., Castelli, M., Garcia-Sanchez, P., Merelo, J.J., Santos, V.M.R., Sim, K. (eds.) Genetic Programming. Lecture Notes in Computer Science, vol. 8599, pp. 137\u2013149. Springer, Berlin (2014)"},{"key":"9409_CR6","volume-title":"Genetic Improvement 2016 Workshop","author":"ZA Kocsis","year":"2016","unstructured":"Kocsis, Z.A., Drake, J.H., Carson, D., Swan, J.: Automatic improvement of Apache Spark queries using semantics-preserving program reduction. In: Petke, J., White, D.R., Weimer, W. (eds.) Genetic Improvement 2016 Workshop. ACM, Denver (2016)"},{"key":"9409_CR7","doi-asserted-by":"crossref","unstructured":"Swan, J., Burles, N.: Chapter Templar\u2014a framework for template-method hyper-heuristics. In: Genetic Programming: 18th European Conference. EuroGP 2015, Copenhagen, Denmark, Proceedings, pp. 205\u2013216. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-16501-1_17"},{"key":"9409_CR8","doi-asserted-by":"crossref","unstructured":"Burles, N., Bowles, E., Brownlee, A.E.I., Kocsis, Z.A., Swan, J., Veerapen, N.: Chapter Object-oriented genetic improvement for improved energy consumption in Google Guava. In: Search-Based Software Engineering: 7th International Symposium. SSBSE 2015, Bergamo, Italy, Proceedings, pp. 255\u2013261. Springer, Cham (2015)","DOI":"10.1007\/978-3-319-22183-0_20"},{"key":"9409_CR9","first-page":"259","volume-title":"Repairing and Optimizing Hadoop hashCode Implementations","author":"ZA Kocsis","year":"2014","unstructured":"Kocsis, Z.A., Neumann, G., Swan, J., Epitropakis, M.G., Brownlee, A.E.I., Haraldsson, S.O., Bowles, E.: Repairing and Optimizing Hadoop hashCode Implementations, pp. 259\u2013264. Springer, Cham (2014)"},{"key":"9409_CR10","doi-asserted-by":"crossref","unstructured":"White, D.R., Joffe, L., Bowles, E., Swan, J.: Deep parameter tuning of concurrent divide and conquer algorithms in Akka. In: Evo-* 2017, LNCS, Porto. Springer, Berin (2017)","DOI":"10.1007\/978-3-319-55792-2_3"},{"key":"9409_CR11","doi-asserted-by":"crossref","unstructured":"Harman, M., Jia, Y., Langdon, W.B.: Babel Pidgin: SBSE can grow and graft entirely new functionality into a real world system. In: Le\u00a0Goues, C., Yoo. S. (eds.) Search-Based Software Engineering, Volume 8636 of Lecture Notes in Computer Science, pp. 247\u2013252. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-09940-8_20"},{"key":"9409_CR12","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A Comprehensive Step-by-Step Guide, 1st edn. Artima Incorporation, Walnut Creek (2008)"},{"key":"9409_CR13","volume-title":"Proofs and Types","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)"},{"issue":"1","key":"9409_CR14","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1109\/TEVC.2013.2281544","volume":"19","author":"WB Langdon","year":"2013","unstructured":"Langdon, W.B., Harman, M.: Optimising existing software with genetic programming. IEEE Trans. Evol. Comput. 19(1), 118\u2013135 (2013)","journal-title":"IEEE Trans. Evol. Comput."},{"key":"9409_CR15","doi-asserted-by":"crossref","unstructured":"Harman, M., Langdon, W.B., Jia, Y., White, D.R., Arcuri, A., Clark, J.A.: The GISMOE challenge: constructing the Pareto program surface using genetic programming to find better programs (keynote). In: ASE, pp. 1\u201314 (2012)","DOI":"10.1145\/2351676.2351678"},{"key":"9409_CR16","doi-asserted-by":"crossref","unstructured":"Ackling, T., Alexander, B., Grunert, I.: Evolving patches for software repair. In: Proceedings of the 13th Annual Conference on Genetic and Evolutionary Computation, GECCO \u201911, pp. 1427\u20131434. ACM, New York (2011)","DOI":"10.1145\/2001576.2001768"},{"issue":"3","key":"9409_CR17","first-page":"149","volume":"26","author":"J-L Krivine","year":"1990","unstructured":"Krivine, J.-L., Parigot, M.: Programming with proofs. J. Inf. Process. Cybern. 26(3), 149\u2013167 (1990)","journal-title":"J. Inf. Process. Cybern."},{"key":"9409_CR18","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA \u201989, pp. 347\u2013359. ACM, New York (1989)","DOI":"10.1145\/99370.99404"},{"key":"9409_CR19","doi-asserted-by":"crossref","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI \u201909, pp. 1\u20132. ACM, New York (2009)","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"9409_CR20","volume-title":"Algebra of Programming. Prentice Hall International Series in Computer Science","author":"RS Bird","year":"1997","unstructured":"Bird, R.S., de Moor, O.: Algebra of Programming. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs (1997)"},{"key":"9409_CR21","unstructured":"Kocsis, Z., Swan, J.: Asymptotic genetic improvement programming with type functors and catamorphisms. In: Workshop on Semantic Methods in Genetic Programming, Parallel Problem Solving from Nature, Ljubljana (2014)"},{"key":"9409_CR22","doi-asserted-by":"crossref","unstructured":"Harman, M., Langdon, W.B., Jia, Y., White, D.R., Arcuri, A., Clark, J.A.: The GISMOE challenge: constructing the Pareto program surface using Genetic Programming to find better programs. In: Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201912) (Keynote), Essen. ACM (2012)","DOI":"10.1145\/2351676.2351678"},{"key":"9409_CR23","unstructured":"Dijkstra, E.W.: On the Reliability of Programs. https:\/\/www.cs.utexas.edu\/~EWD\/transcriptions\/EWD03xx\/EWD303.html , circulated privately(n.d.). Accessed 6 Nov 2015"},{"key":"9409_CR24","doi-asserted-by":"crossref","unstructured":"Qi, Z., Long, F., Achour, S., Rinard, M.: An analysis of patch plausibility and correctness for generate-and-validate patch generation systems. In: Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, pp. 24\u201336. ACM, New York (2015)","DOI":"10.1145\/2771783.2771791"},{"key":"9409_CR25","doi-asserted-by":"crossref","unstructured":"Qi, Y., Mao, X., Lei, Y., Dai, Z., Wang, C.: The strength of random search on automated program repair. In: Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, pp. 254\u2013265. ACM, New York (2014)","DOI":"10.1145\/2568225.2568254"},{"key":"9409_CR26","doi-asserted-by":"crossref","unstructured":"Weimer, W., Fry, Z.P., Forrest, S.: Leveraging program equivalence for adaptive program repair: models and first results. In: Automated Software Engineering (ASE), 2013 IEEE\/ACM 28th International Conference on, pp. 356\u2013366 (2013)","DOI":"10.1109\/ASE.2013.6693094"},{"key":"9409_CR27","unstructured":"White, D.R.: Genetic Programming for Low-Resource Systems, Ph.D. thesis. University of York (2009)"},{"issue":"1","key":"9409_CR28","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"C Goues Le","year":"2012","unstructured":"Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: GenProg: a generic method for automatic software repair. IEEE Trans. Softw. Eng. 38(1), 54\u201372 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"9409_CR29","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1145\/321992.322002","volume":"24","author":"PD Summers","year":"1977","unstructured":"Summers, P.D.: A methodology for LISP program construction from examples. J. ACM 24(1), 161\u2013175 (1977)","journal-title":"J. ACM"},{"key":"9409_CR30","doi-asserted-by":"crossref","unstructured":"Kitzelmann, E.: Inductive programming: a survey of program synthesis techniques. In: Schmid, U., Kitzelmann, E., Plasmeijer, R. (eds.) Approaches and Applications of Inductive Programming, Volume 5812 of Lecture Notes in Computer Science, pp. 50\u201373. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11931-6_3"},{"key":"9409_CR31","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Software Engineering, 2010 ACM\/IEEE 32nd International Conference on, vol. 1, pp. 215\u2013224 (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"9409_CR32","doi-asserted-by":"crossref","unstructured":"Mandelin, D., Xu, L., Bod\u00edk, R., Kimelman, D.: Jungloid mining: helping to navigate the API jungle. In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, pp. 48\u201361 (2005)","DOI":"10.1145\/1065010.1065018"},{"issue":"6","key":"9409_CR33","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1145\/2345156.2254098","volume":"47","author":"D Perelman","year":"2012","unstructured":"Perelman, D., Gulwani, S., Ball, T., Grossman, D.: Type-directed completion of partial expressions. SIGPLAN Not. 47(6), 275\u2013286 (2012)","journal-title":"SIGPLAN Not."},{"key":"9409_CR34","first-page":"418","volume-title":"Computer Aided Verification, Volume of 6806 Lecture Notes in Computer Science","author":"T Gvero","year":"2011","unstructured":"Gvero, T., Kuncak, V., Piskac, R.: Interactive synthesis of code snippets. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification, Volume of 6806 Lecture Notes in Computer Science, pp. 418\u2013423. Springer, Berlin (2011)"},{"key":"9409_CR35","doi-asserted-by":"crossref","unstructured":"Katayama, S.: An analytical inductive functional programming system that avoids unintended programs. In: Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, PEPM \u201912, pp. 43\u201352. ACM, New York (2012)","DOI":"10.1145\/2103746.2103758"},{"key":"9409_CR36","unstructured":"Augustsson, L.: Djinn, a Theorem Prover in Haskell, for Haskell. http:\/\/hackage.haskell.org\/package\/djinn (2005)"},{"issue":"1","key":"9409_CR37","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1023\/A:1005099619660","volume":"60","author":"R Dyckhoff","year":"1998","unstructured":"Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Stud. Log. 60(1), 107\u2013118 (1998)","journal-title":"Stud. Log."},{"key":"9409_CR38","doi-asserted-by":"crossref","unstructured":"Bruce, K.B., Longo, G.: Provable isomorphisms and domain equations in models of typed languages. In: STOC: ACM Symposium on Theory of Computing (STOC) (1985)","DOI":"10.1145\/22145.22175"},{"issue":"2","key":"9409_CR39","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1017\/S0960129500001444","volume":"2","author":"KB Bruce","year":"1991","unstructured":"Bruce, K.B., Di Cosmo, R., Longo, G.: Provable isomorphisms of types. Math. Struct. Comput. Sci. 2(2), 231\u2013247 (1991)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9409_CR40","doi-asserted-by":"crossref","unstructured":"Rittri, M.: Using types as search keys in function libraries. In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA \u201989, pp. 174\u2013183. ACM, New York (1989)","DOI":"10.1145\/99370.99384"},{"key":"9409_CR41","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1017\/S0956796800000861","volume":"3","author":"R Cosmo Di","year":"1993","unstructured":"Di Cosmo, R.: Deciding type isomorphisms in a type-assignment framework. J. Funct. Program. 3, 485\u2013525 (1993)","journal-title":"J. Funct. Program."},{"key":"9409_CR42","volume-title":"Categories for Software Engineering","author":"JL Fiadeiro","year":"2005","unstructured":"Fiadeiro, J.L.: Categories for Software Engineering. Springer, Berlin (2005)"},{"key":"9409_CR43","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1524.001.0001","volume-title":"Basic Category Theory for Computer Scientists","author":"BC Pierce","year":"1991","unstructured":"Pierce, B.C.: Basic Category Theory for Computer Scientists. MIT Press, Cambridge (1991)"},{"issue":"2","key":"9409_CR44","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1162\/evco.1995.3.2.199","volume":"3","author":"DJ Montana","year":"1995","unstructured":"Montana, D.J.: Strongly typed genetic programming. Evol. Comput. 3(2), 199\u2013230 (1995)","journal-title":"Evol. Comput."},{"issue":"2","key":"9409_CR45","doi-asserted-by":"crossref","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. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"9409_CR46","unstructured":"Martin-L\u00f6f, P., Sambin, G.: Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, Napoli (1984)"},{"key":"9409_CR47","unstructured":"Swan, J., Epitropakis, M.G., Woodward, J.R.: Gen-O-Fix: An Embeddable Framework for Dynamic Adaptive Genetic Improvement Programming. Technical Report CSM-195, University of Stirling (2014)"},{"key":"9409_CR48","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1093\/oso\/9780198537618.003.0004","volume-title":"Handbook of Logic in Computer Science","author":"LC Paulson","year":"1992","unstructured":"Paulson, L.C.: Designing a theorem prover. In: Abramsky, S., Gabbay, D.M., Maibaum, S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 415\u2013475. Oxford University Press, New York (1992)"},{"key":"9409_CR49","doi-asserted-by":"crossref","unstructured":"Burmako, E.: Scala macros: let our powers combine! In: Proceedings of the 4th Workshop on Scala, SCALA \u201913, pp. 3:1\u20133:10. ACM, New York (2013)","DOI":"10.1145\/2489837.2489840"},{"key":"9409_CR50","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3"},{"issue":"3","key":"9409_CR51","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(86)90059-1","volume":"22","author":"RJM Hughes","year":"1986","unstructured":"Hughes, R.J.M.: A novel representation of lists and its application to the function \u201creverse\u201d. Inf. Process. Lett. 22(3), 141\u2013144 (1986)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"9409_CR52","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1017\/S0956796805005769","volume":"16","author":"R Hinze","year":"2006","unstructured":"Hinze, R., Paterson, R.: Finger trees: a simple general-purpose data structure. J. Funct. Program. 16(2), 197\u2013217 (2006)","journal-title":"J. Funct. Program."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9409-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9409-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9409-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,22]],"date-time":"2024-06-22T21:21:20Z","timestamp":1719091280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9409-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,7]]},"references-count":52,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["9409"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9409-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,7]]}}}