{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:51:07Z","timestamp":1742921467413,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_11","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"127-141","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Inductive Prover Based on Equality Saturation for a Lazy Functional Language"],"prefix":"10.1007","author":[{"given":"Sergei","family":"Grechanik","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"unstructured":"Graphsc source code and the test suite. https:\/\/github.com\/sergei-grechanik\/supercompilation-hypergraph","key":"11_CR1"},{"issue":"1","key":"11_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796801004191","volume":"12","author":"A Abel","year":"2002","unstructured":"Abel, A., Altenkrich, T.: A predicative analysis of structural recursion. J. Funct. Program. 12(1), 1\u201341 (2002)","journal-title":"J. Funct. Program."},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013)"},{"issue":"3","key":"11_CR4","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM: J. ACM 52(3), 365\u2013473 (2005)","journal-title":"JACM: J. ACM"},{"issue":"4","key":"11_CR5","doi-asserted-by":"publisher","first-page":"1055","DOI":"10.1109\/TKDE.2003.1209024","volume":"5","author":"A Dovier","year":"2003","unstructured":"Dovier, A., Piazza, C.: The subgraph bisimulation problem. IEEE Trans. Knowl. Data Eng. 5(4), 1055\u20131056 (2003). Publisher: IEEE, USA","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"11_CR6","first-page":"48","volume-title":"Proceedings of the Third International Valentin Turchin Workshop on Metacomputation","author":"SA Grechanik","year":"2012","unstructured":"Grechanik, S.A.: Overgraph representation for multi-result supercompilation. In: Klimov, A., Romanenko, S. (eds.) Proceedings of the Third International Valentin Turchin Workshop on Metacomputation, pp. 48\u201365. Ailamazyan University of Pereslavl, Pereslavl-Zalessky (2012)"},{"doi-asserted-by":"crossref","unstructured":"Hamilton, G.W.: Distillation: extracting the essence of programs. In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61\u201370. ACM Press, New York (2007)","key":"11_CR7","DOI":"10.1145\/1244381.1244391"},{"unstructured":"Klyuchnikov, I.: Supercompiler HOSC 1.0: under the hood. Preprint 63, Keldysh Institute of Applied Mathematics, Moscow (2009)","key":"11_CR8"},{"unstructured":"Klyuchnikov, I.: Towards effective two-level supercompilation. Preprint 81, Keldysh Institute of Applied Mathematics (2010). http:\/\/library.keldysh.ru\/preprint.asp?id=2010-81&lg=e","key":"11_CR9"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-11486-1_17","volume-title":"Perspectives of Systems Informatics","author":"I Klyuchnikov","year":"2010","unstructured":"Klyuchnikov, I., Romanenko, S.: Proving the equivalence of higher-order terms by means of supercompilation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 193\u2013205. Springer, Heidelberg (2010)"},{"unstructured":"Klyuchnikov, I., Romanenko, S.: Towards higher-level supercompilation. In: Second International Workshop on Metacomputation in Russia (2010)","key":"11_CR11"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-29709-0_19","volume-title":"Perspectives of Systems Informatics","author":"I Klyuchnikov","year":"2012","unstructured":"Klyuchnikov, I., Romanenko, S.A.: Multi-result supercompilation as branching growth of the penultimate level in metasystem transitions. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 210\u2013226. Springer, Heidelberg (2012)"},{"unstructured":"Lisitsa, A., Webster, M.: Supercompilation for equivalence testing in metamorphic computer viruses detection. In: Proceedings of the First International Workshop on Metacomputation in Russia (2008)","key":"11_CR13"},{"issue":"2","key":"11_CR14","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. JACM: J. ACM 27(2), 356\u2013364 (1980)","journal-title":"JACM: J. ACM"},{"issue":"2","key":"11_CR15","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1145\/227699.227716","volume":"18","author":"D Sands","year":"1996","unstructured":"Sands, D.: Total correctness by local improvement in the transformation of functional programs. ACM Trans. Program. Lang. Syst. 18(2), 175\u2013234 (1996)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"11_CR16","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1017\/S0956796800002008","volume":"6","author":"M S\u00f8rensen","year":"1993","unstructured":"S\u00f8rensen, M., Gl\u00fcck, R., Jones, N.: A positive supercompiler. J. Funct. Program. 6(6), 811\u2013838 (1993)","journal-title":"J. Funct. Program."},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-642-22110-1_59","volume-title":"Computer Aided Verification","author":"M Stepp","year":"2011","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 737\u2013742. Springer, Heidelberg (2011)"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/1594834.1480915","volume":"44","author":"R Tate","year":"2009","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. SIGPLAN Not. 44, 264\u2013276 (2009)","journal-title":"SIGPLAN Not."},{"issue":"3","key":"11_CR19","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/5956.5957","volume":"8","author":"V Turchin","year":"1986","unstructured":"Turchin, V.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(3), 292\u2013325 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T11:17:56Z","timestamp":1674904676000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}